The Community for Technology Leaders
Green Image
<p>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.</p>
Ashrak M. Salem, Laurence V. Pierre, Dominique D. Borrione, "Formal Verification of VHDL Descriptions in the Prevail Environment", IEEE Design & Test of Computers, vol. 9, no. , pp. 42-56, April/June 1992, doi:10.1109/54.143145
90 ms
(Ver 3.3 (11022016))