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.
