Gate-level Approximate Equivalence Checking

Description

Industrial design flows for electronic circuits typically include at least one step of optimization. During this step, the circuit is analyzed and modified in order to improve some specific characteristic, such as speed, size or power consumption, without modifying its logic behavior. Woefully, exact-by-constructions optimization methods can not be always applicable and frequently designers need to validate the correctness of the optimization process by verifying the equivalence between the optimized design and the original one.

Nowadays, state-of-the-art sequential optimization techniques, like sequential redundancy removal, can handle designs with up to hundreds of flip-flops; however, traditional OBDD-based techniques easily run into memory explosion when trying to verify the equivalence of such designs. Several researchers tried to improve the effectiveness of BDD-based verification tools in many different ways: performing verification in stages; identifying equivalent flip-flops pairs for cutting down the search space; adopting ATPG techniques like backward justification; performing approximate state traversals based on a state space decomposition.

However, in many real cases, calculations needed by BDD-based algorithms remain infeasible for the required amount of memory. Moreover, exact methods are usually not able to provide any result if interrupted during execution, and traditional OBDD-based tools can not provide any result if the algorithm is halted in case of memory explosion. Thus, industries can be interested in new verification methodologies that are not exact, but that are always able to produce a result, even though with different levels of confidence.

We propose a new verification methodology, based on a Genetic Algorithm. The proposed approach sacrifices the exactness of the verification in order to gain the ability to handle large designs and to give the designer the opportunity to trade off CPU time with confidence on the result.

This approach should not be considered as a replacement for exact verification tools, but as a complement. But when the complexity of the circuits prevents the use of BDD-based algorithms, we are still able to provide meaningful results.

Papers

Papers dealing with Evolutionary Algorithms and Equivalence Checking.
  1. Evolutionary Simulation-Based Validation
    F. Corno, M. Sonza Reorda, G. Squillero
    International Journal on Artificial Intelligence Tools (IJAIT), Vol. 14, 1-2, Dec. 2004, pp. 897 916
  2. Simulation-Based Sequential Equivalence Checking of RTL VHDL
    F. Corno, M. Sonza Reorda, G. Squillero
    ICECS99: 6th IEEE International Conference on Electronics, Circuits and Systems, Paphos, Cyprus, September 1999, pp. 351-354
  3. Verifying the Equivalence of Sequential Circuits with Genetic Algorithms
    F. Corno, M. Sonza Reorda, G. Squillero
    CEC99: 1999 Congress on Evolutionary Computation, Washington DC (USA), July 1999, pp. 1293-1297
  4. Approximate Equivalence Verification for Protocol Interface Implementation via Genetic Algorithms
    F. Corno, M. Sonza Reorda, G. Squillero
    EuroEcTel99: R. Poli, H-M. Voigt, S. Cagnoni, D. Corne, G. Smith, T. Fogarty (eds.), Evolutionary Image Analysis, Signal Processing and Telecommunications First European Workshops, EvoIASP'99 and EuroEcTel'99 Goteborg, Sweden, May 1999 Joint Proceedings, Springer LNCS, 1999, pp. 182-192
    Special Jury Award for Outstanding Work Presented by a Student or Young Researcher
  5. Approximate Equivalence Verification of Sequential Circuits via Genetic Algorithms
    F. Corno, M. Sonza Reorda, G. Squillero
    DATE99: IEEE Design, Automation & Test in Europe, Munich (Germany), March 1999, pp. 754-755
  6. VEGA: A Verification Tool Based on Genetic Algorithms
    F. Corno, M. Sonza Reorda, G. Squillero
    ICCD98, International Conference on Circuit Design, Austin, Texas (USA), October 1998, pp. 321-326

Contact information

Giovanni Squillero
Politecnico di Torino
Dipartimento di Automatica e Informatica
Corso Duca degli Abruzzi 24
I-10129 Torino
ITALY
Tel: +39-011564.7186
Fax: +39-011564.7099
E-mail: giovanni . squilleroat polito.it
Personal web page: http://staff.polito.it/giovanni.squillero/
Politecnico info page: http://www.dauin.polito.it/en/personale/scheda/(matricola)/003584