Close

Presentation

AutoSVA: Democratizing Formal Verification of RTL Module Interactions
TimeWednesday, December 8th10:30am - 10:52am PST
Location3016
Event Type
Research Manuscript
Virtual Programs
Presented In-Person
Keywords
Design Verification and Validation
Topics
EDA
DescriptionModern SoC design relies on the ability to separately verify IP blocks relative to their own specifications. Formal verification (FV) using SystemVerilog Assertions (SVA) is an effective method to exhaustively verify blocks at unit-level. Unfortunately, FV has a steep learning curve and requires engineering effort that discourages hardware designers from using it during RTL module development. We propose AutoSVA, a framework to automatically generate FV testbenches that verify liveness and safety of control logic involved in module interactions. We demonstrate AutoSVA's bug discovery and verification efficiency by evaluating it on deadlock-critical modules of widely-used open-source hardware projects.