Formal verification is a well-accepted technology for block-level verification, and it's now moving up to the system-on-chip (SoC) level. That's the message behind two paper sessions and two poster presentations at the recent DVCon 2014 conference.
The two paper sessions - which I attended - presented formal verification "apps" for SoC memory map and SoC register map verification. The poster sessions presented apps for security path verification and connectivity verification. This blog post includes three short video interviews with paper presenters. The papers themselves are available now to conference attendees, and will be publicly available at the DVCon web site after April 24, 2014.
A formal app has several defining characteristics. First, it is a tool capability or methodology focused on a specific, high-value problem. Secondly, it doesn't require PhD-level formal verification experience, and most formal apps provide some sort of automatic assertion generation, as well as customized debug views. In addition to running much faster than simulation, formal apps provide exhaustive checks that expose corner-case bugs simulation might miss.
Marvell and Cadence -- Verifying SoC Register Maps
One of the two session papers noted above is titled "Leveraging Formal to Verify SoC Register Map" (12.2). Authors are Abdul Elaydi, senior engineering design manager at Marvell, and Jose Barandiaran, senior member of consulting staff, Cadence.
Elaydi presented the paper and began by noting that comprehensive register verification is very challenging. It requires a system-level environment, which needs more time to set up. Simulation is slow and it is not exhaustive. It is difficult to hit corner cases at the system level.
Marvell worked with Cadence to develop a formal verification flow for a register map. The flow takes an IP-XACT (IEEE 1685-2009) description of the register map that's generated from the register documentation. Leveraging the Cadence Incisive Enterprise Verifier tool, the flow generates assertions to verify register access policies. Typical turnaround time is on the order of "minutes" per check.
The new flow, Elaydi said, is very easy to set up, and verification can start as soon as the documentation is ready. Only a minimal setup is required, and maintenance is easy, because there is no testbench to modify or tests to rewrite. But the biggest benefit, he said, is the exhaustive nature of the formal checking. Using the flow, Marvell engineers found a number of design-versus-specification mismatches.
In the video clip below Elaydi discusses the challenges of SoC register validation, how formal technology helps, advantages of formal versus simulation, and the confidence level (95% or higher) engineers experience in register verification - very nearly replacing simulation for this task.
If video fails to open, click here.
TI and Cadence - Memory Map Verification
The second paper I'll describe here is titled "Accelerated, High-Quality SoC Memory Map Verification Using Formal Techniques" (11.3). It has Texas Instruments and Cadence authors, and was presented by Rajesh Kedia of TI India. Before adopting a formal flow, he noted, TI verified SoC memory maps using system-level tests written in C or assembly language. These checks were not exhaustive, and they took considerable time to develop, simulate, and debug.
The formal flow uses off-the-shelf assertion-based verification IP (ABVIP) from Cadence. ABVIPs are hooked up to selected masters and slaves. Properties in the ABVIPs could be assertions or constraints. In addition, engineers develop some additional custom assertions. Protocol assertions and SoC memory map assertions are then run in the Incisive Formal Verifier (IFV).
In an example with a complex SoC, three critical bugs were caught using this flow. It took just 16 hours to run around 1,300 protocol and memory map assertions. However, the paper also noted some challenges in scaling formal verification up to the SoC level. It is important to limit the state space of the design (by black-boxing modules), choose the right formal engine in IFV, and recognize that certain constraints need to be defined for the memory map to be seen by all masters.
Poster Session: Verifying a Security Path
The poster session was packed wall-to-wall, and I had to squeeze through the crowd to get to a particular paper I wanted to see. Titled "Checking Security Path with Formal Verification Tool: New Application Development" (1P.3), it has STMicroelectronics and Cadence authors and was presented by Jose Barandiaran.
The paper describes a formal app that was developed because STMicroelectronics was concerned about the security of sensitive data in a chip developed by their set-top-box division. The "sensitive data" involves the keys used to decrypt data streams provided to consumer cable and satellite products. The paper compares three approaches that were considered to solve this problem, notes that security path verification was successfully applied on three different paths, and describes a prototype formal app that came out of this collaboration.
In the video clip below, Barandiaran describes the three approaches (symbolic, miter, and x-propagation) and discusses the results of this effort. If video fails to open, click here.
Poster Session: Verifying SoC Connectivity
The final paper I'll mention here is titled "Connecting the Dots: Application of Formal Verification for SoC Connectivity" (1P.20). It was presented in the poster session by Bin Ju, staff application engineer at Cadence. The paper notes that top-level connectivity is complex and difficult to verify with simulation. It lends itself well to formal verification, but customers have found manual creation of assertions to be difficult.
The paper describes a formal verification flow that captures the connectivity specification, exports it as a .csv file, imports it to IFV, generates connectivity assertions, generates a black box module list, executes assertions in IFV, and debugs connectivity failures. The flow is easy to set up and use, and was able to find real bugs that directed tests would not have found (sound familiar by now?). The video below explains further. If video fails to open, click here.
In conclusion, I would say that formal "apps" represent one of the most exciting technology developments in functional verification. And DVCon 2014 provided an excellent venue for learning more about them.
Other Cadence DVCon 2014 Blog Coverage
Jim Hogan at DVCon 2014: Functional Verification Faces "Abundant Chaos" from New Technologies
DVCon 2014 Panel: Did We Create the Functional Verification Gap?
Lip-Bu Tan at DVCon 2014: EDA/Silicon Ecosystem Crucial to Innovation
DVCon 2014 in Review: Formal Verification, Value Chain, and the Industry's Future
DVCon 2014 Video: For Improved Verification, Think About the Flow
DVCon 2014: What's the Missing Piece in Verification?
DVCon 2014 Video: HP Engineers Apply "Test Driven Development" to UVM-e