Hardware Modeling Using Function Encapsulation

Jun Sawada Warren A. Hunt, Jr.

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


We describe how to specify an executable behavioral model of hardware without specifying the hardware detail using ACL2 encapsulation. ACL2 encapsulation is a mechanism to introduce abstract functions with constraints. It can be used to specify a microarchitectural design of hardware, which can be used for early simulation and for verification. Such a high-level design can also be used as a reference model when implementing low-level designs in RTL. This paper examines two abstract specifications used in a microprocessor verification project. One example is a branch predictor for a pipelined machine with speculative execution, and the other is a pipelined execution unit for multiply instructions.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems