Formal Verification of Verilog HDL with Yosys-SMTBMC

Presented at 33C3 (2016), Dec. 28, 2016, 5:15 p.m. (60 minutes).

Yosys is a free and open source Verilog synthesis tool and more. It gained prominence last year because of its role as synthesis tool in the Project IceStorm FOSS Verilog-to-bitstream flow for iCE40 FPGAs. This presentation however dives into the Yosys-SMTBMC formal verification flow that can be used for verifying formal properties using bounded model checks and/or temporal induction. Yosys is a free and open source Verilog synthesis tool and more. It gained prominence last year because of its role as synthesis tool in the Project IceStorm FOSS Verilog-to-bitstream flow for iCE40 FPGAs. This presentation however dives into the Yosys-SMTBMC formal verification flow that can be used for verifying formal properties using bounded model checks and/or temporal induction. Unlike FPGA synthesis, there are no free-to-use formal verification tools available and licenses for commercial tools cost far more than most hobbyists or even small design companies can afford. While IceStorm was the first complete free-as-in-free-speech synthesis tool-chain, Yosys-SMTBMC is the first free Verilog verification flow for any definition of the word "free". Because of the prohibiting pricing of commercial tools it can be expected that most audience members never had a chance to work with formal verification tools. Therefore a large portion of the presentation is dedicated to introducing basic concepts related to formal verification of digital designs and discussing small code examples.

Presenters:

• Clifford

Links:

• https://fahrplan.events.ccc.de/congress/2016/Fahrplan/events/7922.html

Similar Presentations:

• 32C3 (2015) / A Free and Open Source Verilog-to-Bitstream Flow for iCE40 FPGAs
• DEF CON China Beta (2018) / From Memory Safety to Non-bypassable Security
• DEF CON 30 (2022) / Exploitation in the era of formal verification: a peek at a new frontier with AdaCore/SPARK