BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
X-LIC-LOCATION:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20211208T164409Z
LOCATION:3016
DTSTART;TZID=America/Los_Angeles:20211208T103000
DTEND;TZID=America/Los_Angeles:20211208T105200
UID:dac_DAC 2021_sess132_RESEARCH181@linklings.com
SUMMARY:AutoSVA: Democratizing Formal Verification of RTL Module Interacti
 ons
DESCRIPTION:Research Manuscript\n\nAutoSVA: Democratizing Formal Verificat
 ion of RTL Module Interactions\n\nOrenes-Vera\n\nModern SoC design relies 
 on the ability to separately verify IP blocks relative to their own specif
 ications. Formal verification (FV) using SystemVerilog Assertions (SVA) is
  an effective method to exhaustively verify blocks at unit-level. Unfortun
 ately, 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 inter
 actions. We demonstrate AutoSVA's bug discovery and verification efficienc
 y by evaluating it on deadlock-critical modules of widely-used open-source
  hardware projects.\n\nTopic: EDA\n\nKeyword: Design Verification and Vali
 dation\n\nVirtual Program: Presented In-Person
END:VEVENT
END:VCALENDAR