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
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Bundy, Alan: The automation of proof by mathematical induction (2001)
- Kaufmann, Matt; Pecchiari, Paolo: Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem (1996)
- Borrione, Dominique: Denotational semantics of a synchronous VHDL subset. (1995)
- Damm, Werner; Josko, Bernhard; Schlör, Rainer: Specification and verification of VHDL-based system-level hardware designs (1995)
- Borrione, Dominique; Pierre, Laurence; Salem, Ashraf: PREVAIL: A proof environment for VHDL descriptions (1992)