zbMATH — the first resource for mathematics

PREVAIL: A proof environment for VHDL descriptions. (English) Zbl 0794.68143
Correct hardware design methodologies, Proc. Adv. Res. Workshop, Turin/Italy 1991, 163-186 (1992).
Summary: [For the entire collection see Zbl 0747.00045.]
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.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
94C12 Fault detection; testing in circuits and networks