M-CHECK: a multiple engine combinational equivalence checker

Author

Reda, Sherief ; Wahba, Ayman ; Sale, Ashraf

Author_Institution

Dept. of Comput. & Syst. Eng., Ain Shams Univ., Cairo, Egypt

Volume

2

fYear

2000

fDate

2000

Firstpage

613

Abstract

Single engine equivalence checkers have been successfully used in efficiently verifying large designs. However, they also showed inefficiency in proving specific types of circuits. New trends tend to combine multiple equivalence checking engines into a single framework, so that they can verify different kinds of designs more efficiently. In this paper, M-CHECK, a multiple engine equivalence checker, is presented. The proposed checker verifies the combinational circuits using three checking engines: Binary Decision Diagram (BDD) engine, Boolean Satisfiability (SAT) engine, and a mixed BDD SAT engine. Also, the tool is capable of iteratively reducing the design through identifying of equivalent node pairs. The results of our methodology are presented on the ISCAS-85 benchmark circuits

Keywords

Boolean functions; binary decision diagrams; circuit analysis computing; combinational circuits; computability; logic design; logic testing; BDD engine; Boolean satisfiability engine; M-CHECK; binary decision diagram engine; combinational circuits; equivalent node pairs identification; mixed BDD SAT engine; multiple engine combinational equivalence checker; Automatic test pattern generation; Binary decision diagrams; Boolean functions; Circuit faults; Combinational circuits; Data structures; Design engineering; Engines; Equivalent circuits; Systems engineering and theory;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 2000. Proceedings. ISCAS 2000 Geneva. The 2000 IEEE International Symposium on

Conference_Location

Geneva

Print_ISBN

0-7803-5482-6

Type

conf

DOI

10.1109/ISCAS.2000.856403

Filename

856403