HDL-based integration of formal methods and CAD tools in the PREVAIL environment

Borrione, D.; Bouamama, H.; Deharbe, D.; Le Faou, C.; Wahba, Ayman;

Abstract


We present an open environment for the integration of formal methods applied to HDL descriptions of circuits. The system currently accepts SMAX[4] and VHDL, and provides equivalence checking, model checking, theorem proving, and automatic diagnosis of simple design errors. After an overview of the system, we discuss the salient features of the common intermediate format, of the diagnosis tools, and of the automatic generation of NQTHM[11] models from VHDL functional descriptions.


Other data

Title HDL-based integration of formal methods and CAD tools in the PREVAIL environment
Authors Borrione, D.; Bouamama, H.; Deharbe, D.; Le Faou, C.; Wahba, Ayman 
Issue Date 1-Jan-1996
Journal Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 
Start page 450
End page 467
Conference Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISBN [3540619372, 9783540619376]
ISSN 03029743
DOI 10.1007/BFb0031827
Scopus ID 2-s2.0-84957717504

Recommend this item

Similar Items from Core Recommender Database

Google ScholarTM

Check



Items in Ain Shams Scholar are protected by copyright, with all rights reserved, unless otherwise indicated.