DAC User Track Best Paper nominee: "How we Verified 5000 Lines of a Complex Multiplexing Code with Three Assertions"

Shown with the corresponding poster, Nalin Nimavat's paper on the formal verification technique of “symbolic variables” (that used my product, Incisive Formal Verifier -- yeah!) was another nominee for the User Track best paper award. If you are involved in verification at all, I sincerely recommend giving this paper a look because the methodology Nalin and co-author Vigyan Singhal used is pretty straight forward to apply to a variety of design styles which you wouldn't think wouldn't work well with formal. In a nutshell, by adding in the symbolic variables -- a/k/a "don't cares" to oversimplify it -- you only need a few assertions for the formal engines to exhaustively solve the problem in minutes vs. the several days it would take a simulation-based, constrained-random stimulus approach days make a dent in the verification.

 

Full paper citation:

 

8U.5 — How we Verified 5000 Lines of a Complex Multiplexing Code with Three Assertions

This paper describes how the formal verification technique of “symbolic variables” was used to dramatically reduce the complexity and number of assertions to formally verify a networking design – in this case study we went from hundreds of assertions down to only 3! In parallel, applying this methodology substantially increased the scalability and decreased the run time of the formal analyses. This paper also covers how adding helper code can exploit the symmetry of the design without modifying a single line in original RTL.

 

Speaker: Nalin Nimavat - Cisco Systems, Inc., San Jose, CA

 

Authors:

Nalin Nimavat - Cisco Systems, Inc., San Jose, CA

Vigyan Singhal - Oski Technology, Inc., Mountain View, CA

 

Done