PREVAIL: A proof environment for VHDL descriptions The authors describe a formal verification environment for proving the equivalence of two VHDL architectures of the same design entity, provided the designer conforms to some restrictions in the description style. For simple bit-level combinational descriptions, the environment calls upon a tautology checker. For parameterized repetitive structures, and designs described at a more abstract level, the descriptions are translated into recursive functions, according to pre-defined templates, and a theorem is generated in a form acceptable by the Boyer-Moore theorem prover. For well identified classes of circuits, the proof is fully automatic.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element