EQU-IITG: A multi-format formal equivalence checker

A. K. Mishra*, A. Chandra

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Proceeding (Non-Journal item)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2011 International Conference on Energy, Automation and Signal, ICEAS - 2011
PublisherIEEE Press
Pages393-398
Number of pages6
ISBN (Electronic)978-1-4673-0136-7
ISBN (Print)978-1-4673-0137-4
DOIs
Publication statusPublished - 28 Dec 2011
Externally publishedYes
Event2011 International Conference on Energy, Automation and Signal, ICEAS - 2011 - Bhubaneswar, Odisha, India
Duration: 28 Dec 201130 Dec 2011

Publication series

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

Conference

Conference2011 International Conference on Energy, Automation and Signal, ICEAS - 2011
Country/TerritoryIndia
CityBhubaneswar, Odisha
Period28 Dec 201130 Dec 2011

Fingerprint

Dive into the research topics of 'EQU-IITG: A multi-format formal equivalence checker'. Together they form a unique fingerprint.

Cite this