An Overview of the DE Hardware Description Language and Its
Application in Formal Verification of the FM9001 Microprocessor

Cuong Chau
ACL2 Seminar
Sep. 23, 2016

Abstract:

DE is an occurrence-oriented description language that permits the
hierarchical definition of Mealy machines in the style of a hardware
description language. The DE language is formally defined by Warren
Hunt in the ACL2 theorem-proving system. The semantics of the DE
language is given by a simulator that, given the current inputs and
current state for a module, will compute the module's outputs and next
state. DE has shown to be a valuable tool in formal specification and
verification of modern hardware designs. In this talk, I will present
an overview of the DE language; illustrate how to use it to formally
specify and verify circuit designs via simple examples; and finally
briefly describe its application in the FM9001 microprocessor
verification, which was originally created by Bishop Brock and Warren
Hunt in the DUAL-EVAL verification system (the precursor of DE that
was developed in the NQTHM theorem-proving system). Our plan for
future work is to specify and verify the correctness of the FM9001
gate-level design using the asynchronous-circuit-oriented
formalization.