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 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Wang, Qian; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Functional verification of high performance adders in \textscCoq (2014)
- 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) ioport
- Damm, Werner; Josko, Bernhard; Schlör, Rainer: Specification and verification of VHDL-based system-level hardware designs (1995)
- Borrione, Dominique D.; Pierre, Laurence V.; Salem, Ashrak M.: Formal Verification of VHDL Descriptions in the Prevail Environment (1992) ioport
- Borrione, Dominique; Pierre, Laurence; Salem, Ashraf: PREVAIL: A proof environment for VHDL descriptions (1992)