Title :
The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor
Author :
Hunt, Warren A., Jr. ; Brock, Bishop C.
Author_Institution :
Computational Logic Inc., Austin, TX, USA
fDate :
29 Aug-1 Sep 1995
Abstract :
We present an introduction to the DUAL-EVAL hardware description language. DUAL-EVAL is a hierarchical, occurrence-oriented simulator for synchronous Mealy machines. We briefly describe the FM9001 microprocessor, whose design has been formally specified with the DUAL-EVAL language and mechanically proved correct with respect to a behavioral specification. The FM9001 has been fabricated as a CMOS ASIC and tested extensively
Keywords :
computer testing; finite automata; formal specification; formal verification; hardware description languages; integrated circuit testing; microprocessor chips; DUAL-EVAL; FM9001 microprocessor; behavioral specification; formal specification; hardware description language; occurrence-oriented simulator; synchronous Mealy machines; verification; Application specific integrated circuits; CMOS logic circuits; Circuit simulation; Circuit testing; Computational modeling; Formal specifications; Hardware design languages; Large scale integration; Mathematical model; Microprocessors;
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.486381
