Circuit Specification, Abstraction, and Reverse Engineering

Presented as part of the 2007 HCSS conference.

Abstract

We are developing the E hardware description language (HDL). E is a hierarchical, occurance-oriented, HDL that is deeply embedded inside of the ACL2 logic. We use E to represent circuits, and we mechanically verify such representations using the ACL2 theorem-proving system. E may be used to directly specify gate-array and FPGAs designs; we verify transistor-level circuits by preprocessing such circuits into E modules. We can verify circuit generator functions, either by symbolic simulation or by induction. We can compare existing circuits represented in E to proposed specifications, and thus we sometimes use E for reverse engineering circuit descriptions.

The semantics of E are specified by an interpreter written in the ACL2 logic. Our semantics includes a crude delay estimator, which may be used to help manage wire delays. We have generalized our hardware specification approach to permit signal variables to represent equations; these specification functions contain a flag that indicates the equation type (Boolean, four-valued, delay, etc.) of their input arguments and output results.

We have used E to verify a number of predefined ALU circuits; these verifications are generally in the form of symbolic executions, but they can involve using the ACL2 theorem prover. We can synthesize verified circuits, such as 64 and 128-bit multipliers, from our circuit specifications. We have defined both edge-triggered and level-sensitive, state-holding primitives. Using these primitives, a user may define and verify multi-clock (derived from one master clock) circuits. Clocks to state-holding primitives may be gated, and the verification of gated-clock circuits is supported.

We present a mechanism to count the number of different behaviors between two circuits. We present two, flawed adders, and we count the number of different behaviors between these adders and a known good adder. We believe that the number of different behaviors can be a useful metric when attempting to discover subtle, possibly induced, flaws.