The Secret Decoder Ring for Formal Analysis

Those of us of a certain age will remember the secret decoder rings promoted by various products and TV shows. They generally used a simple substitution code to map letters to numbers. According to Wikipedia these have been offered as recently as 2000, so perhaps they are known to younger readers as well. What’s germane to today’s blog post is that formal services company Oski Technology has cleverly used this device as a graphical element in promoting its “Decoding Formal” Club series.

I’ve reported before from these events, which I believe have been very effective at advocating for formal analysis, sharing tricks and techniques, and demystifying what was once regarded as an arcane academic approach to verification. Last week I attended another Decoding Formal Club forum and, as usual, was impressed by the depth of the presentations. Since formal is always a popular topic among readers of The Breker Trekker, I’m going to share a few highlights from that afternoon.

After a brief welcome, the first talk was “Mobile Hardware Security” from Vikas Chandra of ARM Research. He discussed the unique challenges for securing mobile devices, noting that the security solutions used for PCs are not the answer. He described a combination of a hardware-supported hypervisor and a trusted execution environment support by ARM’s TrustZone technology. There are opportunities for formal to verify parts of this solution, but my main reaction is that graph-based scenario models would be a great fit to this system-level hardware/software approach.

Oski’s Prashant Aggarwal presented “How to Ensure the Completeness of End-to-End Formal for Sign-Off” and touched on many aspects of what makes their methodology unique. They focus on “end-to-end” formal properties that verify an entire design block rather than just the assertions inserted in RTL by designers. Their notion of “formal sign-off” and of verifying a block 100% without simulation is rigorously defined and one that they have discussed in previous events. This time they added management of proof depth and deliberate insertion of RTL faults for “negative testing” purposes.

Prashant also presented the results of the “Break the Testbench Challenge” from the Design Automation Conference (DAC) in June. Visitors to the Oski booth were invited to insert bugs into the RTL for an 8×8 multicast crossbar switch design. He described some of the properties in place to try to catch these bugs, including both end-to-checks and internal RTL assertions. A total of 73 bugs were inserted; formal found all of them with the end-to-end properties but only 22 were detected by the RTL assertions.

A real-world example of applying end-to-end checkers and formal sign-off was discussed in “Creative Formal Techniques to Verify PCache” by Kenny Xing from Broadcom, previously shown in a poster session at DAC. The cache in question was fully associative with a FIFO replacement policy, two types of requests, blocks of sequential requests, ability to drop certain requests, and other features that required significant adaptation of traditional verification methods.

I was especially intrigued by the detailed explanation of how the “Wolper Coloring Technique” was modified. The general approach was covered in Prashant’s talk because it was used in the challenge design to ensure that data was not dropped, duplicated, reordered, or corrupted. Since the Broadcom chip could drop requests under specific circumstances, the properties were changed to allow this behavior. I can imagine this coloring technique working for graph-based verification as well, and plan to explore it in more detail in a future blog post.

The final presentation was based on a talk given at the Formal Methods in Computer-Aided Design (FMCAD) conference in September. Yogesh Mahajan of NVDIA and Oski CEO Vigyan Singhal discussed “Compositional Reasoning Gotchas in Practice” and it was an eye-opener for me. The “assume-guarantee” method is commonly used in formal analysis. Consider a master and slave block interconnected by some sort of bus. Properties on the master block’s outputs may be formally proven using a set of assumptions about the inputs coming from the slave block. Conversely, the slave block’s outputs can be verified using assumptions on the inputs from the master.

In practice, it is not always safe to infer that the composition of the two blocks is correct based purely on these two results. This talk showed an example of a deadlock bug that would not be detected without the application of a deeper compositional reasoning rule. There was also a section on the use of safety (bounded) vs. liveness (“eventually”) properties and how improper usage can miss certain bugs. The final topic was dead-end analysis, an important consideration for graphs as well.

Once again Oski put on a stimulating yet pleasant forum. The Computer History Museum is always a nice venue for industry events, and after the meeting we had time to see the new exhibit on self-driving cars. I encourage anyone who’s serious about formal analysis to consider attending in the future, and I expect to see you there!

Tom A.

The truth is out there … sometimes it’s in a blog.

Tags: Accellera, ARM, assertions, Breker, Broadcom, cache coherency, constraints, EDA, formal, functional verification, graph-based verification, NVIDIA, oski, portable stimulus, properties, scenario model, SoC verification, standards, Trek, TrekApp, TrekSoC

This entry was posted on Wednesday, October 28th, 2015 at 6:19 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.