Title :
A prover for VHDL-based hardware design
Author_Institution :
Integrierte Hardware-Software-Syst., OFFIS, Oldenburg, Germany
fDate :
29 Aug-1 Sep 1995
Abstract :
Surveys a self-contained part of the ESPRIT-project “FORMAT”, which develops a prover for VHDL-based hardware design. Notable is the use of a graphical specification language called STD (Symbolic Timing Diagrams), which can be seen as a visual dialect of temporal logic. The heart of the prover is built by two powerful industrial verification tools: A (compositional) symbolic model checker (developed by SIEMENS), and the LAMBDA-theorem prover (developed by AHL). The aim of this paper is to describe (1) the various tools integrated in the prover, (2) the graphical specification language STD with its associated design methodology, and (3) to explain how proofs about generic (parameterized) designs are performed in the prover, using a combination of automatic and interactive reasoning
Keywords :
hardware description languages; logic CAD; logic testing; temporal logic; theorem proving; LAMBDA-theorem prover; STD; Symbolic Timing Diagrams; VHDL; graphical specification language; hardware design; symbolic model checker; temporal logic; verification tools; Design methodology; Hardware; Heart; Logic; Performance analysis; Protocols; Sliding mode control; Specification languages; Timing; Visual databases;
Conference_Titel :
Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL '95/VLSI '95., IFIP International Conference on Hardware Description Languages. IFIP International Conference on Very Large Scal
Conference_Location :
Chiba
Print_ISBN :
4-930813-67-0
DOI :
10.1109/ASPDAC.1995.486382
