AutoSVA: Democratizing Formal Verification of RTL Module Interactions

Marcelo Orenes-Vera, Aninda Manocha, David Wentzlaff, Margaret Rose Martonosi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication2021 58th ACM/IEEE Design Automation Conference, DAC 2021
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages535-540
Number of pages6
ISBN (Electronic)9781665432740
DOIs
StatePublished - Dec 5 2021
Event58th ACM/IEEE Design Automation Conference, DAC 2021 - San Francisco, United States
Duration: Dec 5 2021Dec 9 2021

Publication series

NameProceedings - Design Automation Conference
Volume2021-December
ISSN (Print)0738-100X

Conference

Conference58th ACM/IEEE Design Automation Conference, DAC 2021
Country/TerritoryUnited States
CitySan Francisco
Period12/5/2112/9/21

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering
  • Modeling and Simulation

Keywords

  • automatic
  • formal
  • modular
  • SVA
  • verification

Fingerprint

Dive into the research topics of 'AutoSVA: Democratizing Formal Verification of RTL Module Interactions'. Together they form a unique fingerprint.

Cite this