Title :
An equivalence checking methodology for hardware oriented C-based specifications
Author :
Saito, Hiroshi ; Ogawa, Takaya ; Sakunkonchak, Thanyapat ; Fujita, Masahiro ; Nanya, Takashi
Author_Institution :
Res. Center for Adv. Sci. & Technol., Univ. of Tokyo, Japan
Abstract :
Verification to validate designs is one of the important tasks in VLSI design flow. Due to the great advances in integration, verification for whole designs is getting more and more difficult. To solve this problem in early stages of design flows, we suggest a formal equivalence checking method for given two C-based hardware oriented specifications (C descriptions). To verify large C descriptions efficiently, we use textual differences in the two C descriptions and verify them in terms, of symbolic simulation. We believe that our approach will be useful where two specifications to be verified are very close, which is a very common situation in practical designs.
Keywords :
C language; VLSI; formal verification; logic CAD; C descriptions; VLSI design; design flows; equivalence checking; formal equivalence checking; hardware specifications; symbolic simulation; verification; Debugging; Design engineering; Feedback; Hardware; High level synthesis; Productivity; Reduced instruction set computing; Resource management; Scheduling; Very large scale integration;
Conference_Titel :
High-Level Design Validation and Test Workshop, 2002. Seventh IEEE International
Print_ISBN :
0-7803-7655-2
DOI :
10.1109/HLDVT.2002.1224443