The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor

Authors: Brock B.C.¹; Hunt Jr. W.A.¹

Source: Formal Methods in System Design, Volume 11, Number 1, July 1997 , pp. 71-104(34)

Publisher: Springer

Key:

- Free Content

- New Content

- Subscribed Content

- Free Trial Content

Abstract:

We present the full formal semantics of 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: Hardware Verification; FM9001; DUAL-EVAL; Microprocessors; Hardware Description Languages

Language: English

Document Type: Regular paper

Affiliations: 1: Computational Logic, Inc. 1717 West Sixth Steet, Suite 290 Austin, TX 78703-4776 U.S.A.; Tel: +1 512 322 9951, FAX: +1 512 322 0656, E-mail: brock@cli.com, hunt@cli.com

The full text electronic article is available for purchase. You will be able to download the full text electronic article after payment.

$42.00 plus tax