Formal Verification of Pipeline Control
AbstractWe 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.