Skip to main content

AutoSVA: Democratizing Formal Verification of RTL Module Interactions

Author(s): Orenes-Vera, Marcelo; Manocha, Aninda; Wentzlaff, David; Martonosi, Margaret

To refer to this page use:
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.
Publication Date: Dec-2021
Citation: Orenes-Vera, Marcelo, Manocha, Aninda, Wentzlaff, David and Martonosi, Margaret. "AutoSVA: Democratizing Formal Verification of RTL Module Interactions." 2021 58th ACM/IEEE Design Automation Conference (DAC) (2021). doi:10.1109/DAC18074.2021.9586118
DOI: 10.1109/DAC18074.2021.9586118
Type of Material: Conference Article
Journal/Proceeding Title: 2021 58th ACM/IEEE Design Automation Conference (DAC)
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.