A prover for VHDL-based hardware design

Author

Schlör, Rainer

Author_Institution

Integrierte Hardware-Software-Syst., OFFIS, Oldenburg, Germany

fYear

1995

fDate

29 Aug-1 Sep 1995

Firstpage

643

Lastpage

650

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ASPDAC.1995.486382

Filename

486382