|
Formal Verification of Pipeline Control
Abstract
We present an semi-formal verification method that can detect common
pipeline-control
bugs of logic-design components containing thousands of registers. The
method models
logic designs as controlled token nets. A controlled token net consists
of
(1) a token net that models the data flow in the datapath using token
semantics and
(2) a control logic that models the control machines using traditional
state
semantics. We provide algorithms to (1) extract a controlled token net
from a logic
design, (2) minimize the controlled token net, and (3) compute an
abstract
interpretation of the controlled token net for efficient model checking
of
controlled token nets. We implemented and applied the method to 6 Intel
logic-design
components containing up to 4500 registers and successfully detected 8
pre-silicon
errata. This is joint work with Adrian Isles and Timothy Kam and was
presented at
the ICCAD conference, 1998.
|