Formal verification of pipeline control using controlled token nets and abstract interpretation

We present an automated formal verification method that can detect common pipeline-control bugs of logic-design components containing thousands of registers. The method models logic designs using controlled token nets. A controlled token net consists of: a token net that models the data flow in the datapath using token semantics; a control logic that models the control machines using traditional finite 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. We implemented and applied the method to 6 Intel logic-design components containing up to 4500 registers and successfully detected 8 pre-silicon errata. 1.1 Keywords Pipeline control verification, controlled token net, abstract interpretation, processor verification, model checking, formal verification, functional verification, computer-aided design 2