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 details on specific features in specific products. Attendance has been good, so I’m pleased with how the series is going.
This approach has also given us the chance to cover some specific topics we’ve only touched on briefly in past webinars. 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. That’s way too many to cover in this post, but I’d like to give some examples and hit a few high points.
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 means that all possible behavior has been mathematically analyzed and 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.
