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:20240626T180033Z
LOCATION:3004\, 3rd Floor
DTSTART;TZID=America/Los_Angeles:20240627T114500
DTEND;TZID=America/Los_Angeles:20240627T120000
UID:dac_DAC 2024_sess135_RESEARCH1175@linklings.com
SUMMARY:Formally Verifying Arithmetic Chisel Designs for All Bit Widths at
  Once
DESCRIPTION:Research Manuscript\n\nWeizhi Feng and Yicheng Liu (Institute 
 of Software, Chinese Academy of Sciences); Jiaxiang Liu (Shenzhen Universi
 ty); and David Jansen, Lijun Zhang, and Zhilin Wu (Institute of Software, 
 Chinese Academy of Sciences)\n\nEfficient verification of ALUs has always 
 been a challenge. Traditionally, they are verified at a low level, leading
  to state space explosion for larger bit widths. We symbolically can verif
 y ALUs for all bit widths at once. \nChisel is a hardware description lang
 uage embedded in Scala. Our key idea is to transform arithmetic Chisel des
 igns into Scala software programs that simulate their behavior, then apply
  Stainless, a deductive formal verification tool for Scala. We validate th
 e effectiveness by verifying dividers and multipliers in two open-source R
 ISC-V processors, and conclude that our approach requires less manual guid
 ance than others.\n\nTopic: EDA\n\nKeyword: Design Verification and Valida
 tion\n\nSession Chair: Nan Wu (University of California, Santa Barbara)
END:VEVENT
END:VCALENDAR