Formal verification of VHDL descriptions in the Prevail environment
- 1 June 1992
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Design & Test of Computers
- Vol. 9 (2) , 42-56
- https://doi.org/10.1109/54.143145
Abstract
Prevail, a formal verification environment for proving the equivalence of two very-high-speed integrated circuit hardware description language (VHDL) design architectures, is described. For simple bit-level combinational descriptions, the environment calls upon a tautology checker. For parameterized repetitive structures and for more abstract sequential designs, the program translates descriptions into recursive functions according to predefined templates and generates a theorem acceptable to the Bover-Moore theorem prover. The specification, implementation, and functional representation of a sequential example are presented.<>Keywords
This publication has 7 references indexed in Scilit:
- Proving circuit correctness using formal comparison between expected and extracted behaviourPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Correctness proofs of parameterized hardware modules in the Cathedral-II synthesis environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Sequential circuit verification using symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verifikation digitaler SystemePublished by Springer Nature ,1991
- Verification of synchronous sequential machines based on symbolic executionPublished by Springer Nature ,1990
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- The denotational semantics of sequential machinesInformation Processing Letters, 1980