@inproceedings{552f89d0a4cd44beb60d6b5afb309be3,
title = "AutoSVA: Democratizing Formal Verification of RTL Module Interactions",
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.",
keywords = "SVA, automatic, formal, modular, verification",
author = "Marcelo Orenes-Vera and Aninda Manocha and David Wentzlaff and Margaret Martonosi",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 58th ACM/IEEE Design Automation Conference, DAC 2021 ; Conference date: 05-12-2021 Through 09-12-2021",
year = "2021",
month = dec,
day = "5",
doi = "10.1109/DAC18074.2021.9586118",
language = "English (US)",
series = "Proceedings - Design Automation Conference",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "535--540",
booktitle = "2021 58th ACM/IEEE Design Automation Conference, DAC 2021",
address = "United States",
}