Formal at System Level. Innovation in Verification

Formal verification at the SoC level has long seemed an unapproachable requirement. Maybe we should change our approach. Could formal be practical on a suitable abstraction of the SoC? Paul Cunningham (GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and now Silvaco CTO) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs. The paper published in the 2014 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. The authors are from the University of Kaiserslautern in Germany.

Though the paper is old, this is a worthy goal and has a respectable number of citations. While there has been limited commercial development, the topic is still unfamiliar to most of us. The authors argue for a different kind of abstraction from familiar methods in conventional formal. They propose Path Predicate Abstraction (PPA). This centers around important states in the stage transition graph and operations which are multicycle transitions between important states.

The paper illustrates top-down construction of an example PPA as an FSM, with macros defining states and properties defining operations as sequences of transitions between states. Macros connect to the RTL implementation through signal name references. They check these formally against the RTL. Further, they show how such an PPA state machine can be proven sound and complete. They claim this demonstrates formally complete coverage on the abstract graph for the SoC.

Paul’s view

This paper is a heavy read but is an important contribution that has been well cited. The concept is easy to appreciate. First create an abstract state machine to describe design functionality at a system level and then prove that an RTL implementation of the design conforms to its abstraction. The abstract state machine is represented as a bunch of temporal logic properties, e.g. System Verilog Assertions (SVAs).

Proving that some RTL conforms to an SVA is of course not new and is not the contribution of the paper. The contribution is a method to prove the reverse: that a set of SVAs completely covers all possible behaviors of some RTL, relative to a particular level of abstraction.

This is a pretty cool concept, and the authors’ open with an elegant way to visualize their approach as a form of coloring of the states in the RTL implementation of a design. They tie off their work with two worked examples – a simple bus protocol and a serial IO data packet framer.

I would have liked to see one of the examples being a compute centric design vs. a protocol centric design. Protocol centric designs always have a clear and obvious system level state machine to verify against, and indeed at Cadence we offer a library of formal protocol proof kits very much along the lines of this paper which we refer to as Assertion-Based Verification IPs (AB-VIPs for short).

But for a compute centric design we’ve found it much harder to represent the intended behavior using assertions and state machines. A sequential equivalence checking approach – either between two versions of RTL or between a C/C++ model and RTL implementation has generally proved to be more scalable.

Raúl’s view

The core concept is to define the semantics of a system model by formulating properties in a standard property language, such as SystemVerilog assertions (SVA). If these properties can be proven using standard property checking techniques, then the system model is a sound abstraction of an RTL design. It is important to note that the objective of the paper is show a method to establish equivalence between an abstraction and the ground RTL. It does not offer innovation in arriving at a sound abstraction, for example finding optimal ways to color the graph.

The proposed methodology is applied to two designs. A flexible peripheral interconnect (FPI) bus with a total of ~16,000 Lines of Code. The number of state bits reduced from over 1500 to just 38, in 1850 lines of code (LoC). A property checker proved all properties in 90 seconds. The authors estimated effort to create a complete set of properties for SoC module verification to be around 2000 LoC per person month, meaning approx. 8-person month in total.

A second example is a SONET/SDH Framer (Table III) of about 27,000 LoC. This shows equally impressive results, reducing the number of state bits from over 47,000 to just 11. The total manual effort including formal verification of 27k LoC in VHDL was about six person months in this case. Properties checked in less than two minutes.

Establishing “sound abstractions” at levels above RTL is key to raise the level of abstraction. The paper is an important contribution in this area. Surprisingly, the cost in term of proving the soundness of these abstractions is negligible, just minutes using a model checker. What is not negligible however, is the non-automated effort of coming up with these abstractions. Many months by experts familiar with the non-trivial methodology. It is also not clear how expressive these abstractions are. The author’s touch on this, “We find this abstract graph by constructing a mapping function… In this context, we may observe that trivial coloring functions always exist that assign every node in the graph a different color or that assign the same color to all nodes (the resulting path predicate abstractions are, of course, meaningless) “. If and how this methodology makes its way into practical design tools is an interesting question.

My view

A note on how I approach math-heavy papers like this. Our primary interest is engineering value so, to first order, I focus on opening proposition, experiments and results. Dense algebraic justification I treat as an appendix, interesting maybe to read later if warranted. This makes for a much easier read!