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

fYear

1995

fDate

29 Aug-1 Sep 1995

Firstpage

637

Lastpage

642

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;

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.486381

Filename

486381