AutoSVA: Democratizing Formal Verification of RTL Module Interactions

TL;DR

AutoSVA is a framework that automates the creation of formal verification testbenches for RTL modules, making formal verification more accessible and efficient for hardware designers.

Contribution

It introduces AutoSVA, a novel system that automatically generates SystemVerilog Assertion-based testbenches for verifying RTL module interactions.

Findings

AutoSVA effectively detects deadlocks in open-source hardware modules.

It reduces the effort required for formal verification in RTL design.

AutoSVA demonstrates high efficiency in verifying control logic safety and liveness.

Abstract

Modern 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 effectiveness and efficiency on deadlock-critical modules of widely-used open-source hardware projects.