A methodology for formal hardware verification based on symbolic trajectory evaluation
Randal E. Bryant, Kyle L. Nelson · 1999
Formal methods refer to a class of techniques used to verify hardware systems. The use of formal methods does not guarantee correctness, instead it reveals inconsistencies, ambiguities, and incompletenesses which might have otherwise been undetected. This thesis focuses on a methodology which enables developers to apply formal methods to the verification of processors. The correct behavior of a processor is based on the architecture's instruction set semantics. The sequencing model inherent to processors is the sequential execution of instructions. Modern processors pose a verification challenge because in an effort to increase performance they deviate from the sequential execution model. Consequently, processors are often composed of largely independent functional units or subsystems which interact together to implement the system's architecture. Our methodology verifies that a processor's functional unit correctly satisfies the system's high-level specification. A subsystems specification contains a high-level specification and an implementation mapping. The high-level specification is in the form of a set of abstract assertions; the implementation mapping relates the abstract assertion to the implementation. It is represented by directed graphs and takes into account such details as the effects of pipelining, clocking, and interfaces with interacting subsystems. Additionally, the mapping must also consider the effects of overlapping instructions in the subsystem. The high-level specification and the implementation mapping are combined to automatically generate a set of low-level assertions which define the subsystem's specification. Each low level assertion is efficiently verified using symbolic trajectory evaluation. The methodology developed in this thesis is applied to the fixed point unit of a processor implementing the PowerPC architecture. The abstract specification was derived from the architecture's instruction set semantics and the implementation mapping is based on the subsystems microarchitecture. Symbolic trajectory evaluation was used to verify that a gate-level representation of the subsystem properly implements its specification.