EQU-IITG: A multi-format formal equivalence checker

A. K. Mishra*, A. Chandra

*Awdur cyfatebol y gwaith hwn

Allbwn ymchwil: Pennod mewn Llyfr/Adroddiad/Trafodion CynhadleddTrafodion Cynhadledd (Nid-Cyfnodolyn fathau)

1 Dyfyniad (Scopus)

Crynodeb

Checking for the functional equivalence between two models of a design is a crucial step in a hierarchical transformation based design flow, in which a designer obtains low level implementation models by manual or automatic translation from higher level specification models. Some of the most difficulty tasks CAD users face are the evaluation, comparison and compatibility-issue for different formats of different EDA tools and algorithms. It is vital to understand how well a given verification tool does the required job and which of the many possible formats can be verified. Formal methods are playing a major role in the verification environment. This paper presents a verification technique for functional comparison of large circuits (combinational and sequential) using a combination of known approaches. The idea is based on the tight integration of structural satisfiability (SAT) solver, BDD sweeping, FSM traversal and random simulation; all four working on a shared graph representation of the circuit. This integral method enhances the performance of BDD verification based on the complexity of the circuit. Further, the random simulation algorithm works on the compressed circuit graph and thus runs more efficiently. The outlined approach is effective for both sequential and combinational circuits. Besides this verification, this tool supports multiple formats for verification, generated through the different stages of design flow. This avoids requirement of another tool for conversion of one format to the other for equivalence checking.

Iaith wreiddiolSaesneg
TeitlProceedings - 2011 International Conference on Energy, Automation and Signal, ICEAS - 2011
CyhoeddwrIEEE Press
Tudalennau393-398
Nifer y tudalennau6
ISBN (Electronig)978-1-4673-0136-7
ISBN (Argraffiad)978-1-4673-0137-4
Dynodwyr Gwrthrych Digidol (DOIs)
StatwsCyhoeddwyd - 28 Rhag 2011
Cyhoeddwyd yn allanolIe
Digwyddiad2011 International Conference on Energy, Automation and Signal, ICEAS - 2011 - Bhubaneswar, Odisha, India
Hyd: 28 Rhag 201130 Rhag 2011

Cyfres gyhoeddiadau

EnwProceedings - 2011 International Conference on Energy, Automation and Signal, ICEAS - 2011

Cynhadledd

Cynhadledd2011 International Conference on Energy, Automation and Signal, ICEAS - 2011
Gwlad/TiriogaethIndia
DinasBhubaneswar, Odisha
Cyfnod28 Rhag 201130 Rhag 2011

Ôl bys

Gweld gwybodaeth am bynciau ymchwil 'EQU-IITG: A multi-format formal equivalence checker'. Gyda’i gilydd, maen nhw’n ffurfio ôl bys unigryw.

Dyfynnu hyn