BEGIN:VCALENDAR VERSION:2.0 PRODID:IEEE vTools.Events//EN CALSCALE:GREGORIAN BEGIN:VTIMEZONE TZID:Europe/Vienna BEGIN:DAYLIGHT DTSTART:20170326T030000 TZOFFSETFROM:+0100 TZOFFSETTO:+0200 RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3 TZNAME:CEST END:DAYLIGHT BEGIN:STANDARD DTSTART:20161030T020000 TZOFFSETFROM:+0200 TZOFFSETTO:+0100 RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10 TZNAME:CET END:STANDARD END:VTIMEZONE BEGIN:VEVENT DTSTAMP:20180128T162204Z UID:FAE6BF88-E03D-47E2-BEC2-7677364667B7 DTSTART;TZID=Europe/Vienna:20170306T130000 DTEND;TZID=Europe/Vienna:20170306T140000 DESCRIPTION:Yosys is a free and open source Verilog synthesis tool and more . In this presentation we discuss Yosys-SMTBMC\, a Yosys-based formal veri fication\nflow that can use any SMT-LIB2 solver as back-end engine\, and S ymbiYosys\, a uniform front-end for various Yosys-based formal flows\, inc luding Yosys-SMTBMC and flows utilizing AIGER-based engines.\n\nSpeaker(s) : Clifford Wolf\, \n\nRoom: S2 Z74\, Bldg: Science Park 2\, Johannes Keple r University Linz\, Altenbergerstr. 69\, Linz\, Oberosterreich\, Austria\, 4040 LOCATION:Room: S2 Z74\, Bldg: Science Park 2\, Johannes Kepler University L inz\, Altenbergerstr. 69\, Linz\, Oberosterreich\, Austria\, 4040 ORGANIZER:andreas.springer@jku.at SEQUENCE:2 SUMMARY:Formal Verification of Verilog HDL with Yosys-SMTBMC and SymbiYosys URL;VALUE=URI:https://events.vtools.ieee.org/m/159602 X-ALT-DESC:Description: <br /><p>Yosys is a free and open source Verilog sy nthesis tool and more. In this presentation we discuss Yosys-SMTBMC\, a Yo sys-based formal verification<br />flow that can use any SMT-LIB2 solver a s back-end engine\, and SymbiYosys\, a uniform front-end for various Yosys -based formal flows\, including Yosys-SMTBMC and flows utilizing AIGER-bas ed engines.</p> END:VEVENT END:VCALENDAR