"A Formalized Verification Methodology for Soft IP Cores in Safety-Critical Applications"

Travis Lenhart and John Lach
University of Virginia

Abstract

While accurate evaluation of the functionality contained within intellectual property (IP) cores (often expressed in a hardware description language such as VHDL or Verilog), is important for all applications, it is absolutely essential when such cores are utilized within applications or systems that are considered safety-critical in nature. This paper presents the development of a semi-formal verification methodology for IP cores based upon a single, unified notation for both simulation and formal verification. Derived largely from an Assertion-Based Verification (ABV) methodology, this formal property checking methodology utilizes the IEEE P1850 Property Specification Language (PSL) to provide a small, simple learning curve for both IP design and IP verification engineers unfamiliar with more complex formal methods (e.g. theorem proving) and a means to combine traditional dynamic verification (i.e. functional simulations) with a rigorous static formal verification method. 

Emphazing the use of static formal property checking and the development of safety properties rather than simulation test vectors, this methodology includes benefits that can be realized throughout all stages of IP development applied towards both existing and newly specified systems. Specification assertions help to formalize the functional requirements contained within the IP specification, while embedded (white-box) assertions and interface (black-box) assertions aid in both the construction and understanding of the IP component implementation and the IP system test implementation, respectively. Development and use of these assertions at all levels of the system hierarchy help to increase both the controllability and observability of the design under verification through improvements in error detection, error isolation, and error notification capabilities. In addition, unlike the simulation test vectors that are typically developed by IP designers for IP component verification and then often not utilized by others, assertions that have been developed as part of this process are not discarded. Rather, serving as verification IP, they are actively coupled with the design IP to act as a reusable interface between the design IP and IP end-users. 

To demonstrate the effectiveness of this methodology, a case study has been developed based upon this ABV methodology using a simple, freely-available IP core of the CPU of a popular 8-bit microcontroller the Motorola 68HC11. Through this case study the functional and temporal correctness of a suite of PSL safety properties and assertions developed from the IP core specification (i.e. data sheet) will be determined. In order to verify implementation-dependent IP design elements that have not been explicitly defined within the specification and to more closely reflect the role of an IP verifier within the IP evaluation process, a set of PSL safety properties and assertions will also be developed directly from the design implementation as expressed using VHDL RTL code. Using the RuleBaseTM formal property checking tool developed by IBM, these sets of assertions will be developed based upon the various elements included within the design hierarchy, such as the individual CPU datapath components, the CPU datapath as a whole, the CPU control unit, and all instructions contained within the ISA. Satisfaction of the defined exit criteria, and therefore the quality of the verification effort, will be measured through the utilization of a functional coverage metric that incorporates coverage of both assertions and other functional coverage points.

2006 MAPLD International Conference Home Page