Specification Automation for Formal Verification

I hope that you’ve been able to attend or watch the recordings of the sessions in our latest webinar series on specification automation. We’re focusing on the requirements for different project teams and different tasks in the system-on-chip (SoC) development process: hardware design, simulation, formal verification, firmware coding, system-level validation, documentation, and more. This approach makes it easy for us to focus on the solutions we provide without digging deeply into the details of specific features in specific products. I’m pleased with how the series is going; attendance has been good. 

This approach has also given us the chance to cover some specific topics we’ve only touched on briefly in past webinars. The generation of assertions for use in formal verification is one such topic. In a recent designer-focused blog post, I mentioned that we generate assertions for clock domain crossings (CDCs), but that barely scratches the surface of our capabilities. In fact, our most recent webinar listed more than 80 categories of assertions that we generate today. I can’t cover all, but let’s touch on key examples and highlights in this post. 

The Power of Formal Verification: A Brief Overview

First, let me remind you how formal verification works. A formal tool takes an assertion—a statement of design intent—and tries to prove that it is true under all possible states of your design. This is much more powerful than simulation, which only exercises the design behavior stimulated by your tests. A formal proof mathematically analyzes all possible behavior, ensuring that the assertion “holds” under all conditions. Of course, your design may have a bug that violates an assertion, and in this case, the formal tool generates a “counterexample” that shows exactly how this can happen.

You can specify constraints to ensure that formal analysis considers only legal design behavior. If you have a two-bit input that must be one-hot, you don’t want to see an invalid counterexample in which both bits are set high. You can also use formal tools to target coverage points. These days, almost everyone uses SystemVerilog Assertions (SVA) to specify assertions (“assert”), constraints (“assume”), and coverage (“cover”). We generate all our assertions in SVA, specifically in the form of concurrent assertions aligned with the clock cycles in your design, and they work in simulation as well as formal.

Automating Assertions: Simplifying Formal Verification Efforts

So, assertions are very powerful, but they do take some effort to write. SVA is a complex language, and often some SystemVerilog “helper code” is needed to set up the assertions properly. Just as with any other aspect of specification automation, the more that we can generate from your specifications the less work you have to do. I mentioned CDC; we automatically detect signals between asynchronous clock domains, generate register-transfer-level (RTL) synchronizers, the SystemVerilog testbench code to verify them in simulation, and the SVA for formal analysis to prove that they are correct.

There are many other cases in which we generate SVA along with the design, testbench code, C/C++ code, and documentation. For example, we check for proper behavior of functional safety logic such as parity, error correcting code (ECC), cyclic redundancy code (CDC), and sniffing engines. We ensure that we have properly generated these RTL structures per your specification, we double-check the mathematical calculations performed, we verify read and write operations, and we check that errors are properly reported.

Of course, we’re best known for register automation, so we generate assertions for registers as well. We check that data is actually read or written and that read-only and write-only fields are used properly. We generate additional SVA for a wide range of special register types, including lock, alias, interrupt, paged, shadow, indirect, and virtual registers, plus FIFOs and counters. The assertions check for proper read and write behavior, including access from both hardware and software and consistency across related registers. You can formally verify every aspect of every register in your design.

Extending Formal Verification to the Chip Level

Assertions are also valuable at the chip level. Formal analysis has capacity limitations, so it is rare for assertions across an entire chip to be proven completely. However, there are some types of top-level assertions, especially those involving connectivity, that run very well in formal tools. As I’ve discussed before, our chip assembly solution generates all the RTL code needed to interconnect blocks from our SLIP-G library of IP generators, as well as your own custom design blocks, in the top level of your chip design. We also generate RTL aggregators, bridges, and multiplexors for standard buses as needed.

We generate SVA in addition to the RTL design and documentation for the top level. We check that all connections across the IP and blocks match your specifications. We generate topology assertions to verify that data transfers properly through the bridges and aggregators. For chips with multiple masters, e.g., in a multi-processor SoC, we verify the arbiter’s correct implementation of your algorithm and data multiplexing. All these assertions can be formally verified in even the largest chips.

Our recent webinar provides more information on our assertions, including specific examples within the general categories I’ve listed here. You can watch any of our recorded webinars, by visiting this page. You can also register to attend upcoming webinars live. We’re pleased to enable easier use of formal verification with our automatically generated SVA. These leverage the same executable specifications that we use to generate design code, testbench code, and documentation. There’s no additional work for you, so there’s no easier way to benefit from the tremendous power of formal technology.