Hardware & Making

Formal Verification of Verilog HDL with Yosys-SMTBMC

Saal 6
Clifford
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.

Additional information

Type lecture
Language English

More sessions

12/27/16
Hardware & Making
Daniel Estévez
Saal 2
<a href="https://outernet.is">Outernet</a> is a company whose goal is to ease worldwide access to internet contents by broadcasting files through geostationary satellites. Most of the software used for Outernet is open source, but the key parts of their receiver are closed source and the protocols and specifications of the signal used are secret. I have been able to <a href="http://destevez.net/tag/outernet/">reverse engineer</a> most of the protocols, and a functional <a ...
12/27/16
Hardware & Making
Saal G
Software Defined Radios (SDRs) became a mainstream tool for wireless engineers and security researches and there are plenty of them available on the market. Most if not all SDRs in the affordable price range are using USB2/USB3 as a transport, because of implementation simplicity. While being so popular, USB has limited bandwidth, high latency and is not really suitable for embedded applications. PCIe/miniPCIe is the only widespread bus which is embedded friendly, low latency and high bandwidth ...
12/27/16
Hardware & Making
ctrapp
Saal 6
The NibbleTronic is a MIDI wind controller that features a novel user interface resulting in a unique tonal range. The standard configuration allows to precisely play a bit more than four full octaves including semitones with only one hand.
12/27/16
Hardware & Making
Hendrik Lüth
Saal G
Mit steigendem Datenaufkommen und einer immer größer werdenden Zahl von Geräten muss auch das WLAN wachsen. Nach "ur WiFi sucks!!1!" ist dieser Talk eine kleine Einführung in die Neuerungen, welche mit dem 802.11ac-Standard gekommen sind und gibt eine Erklärung, wie sie funktionieren.
12/27/16
Hardware & Making
Ray
Saal 1
"Smart" devices using BTLE, a mobile phone and the Internet are becoming more and more popular. We will be using mechanical and electronic hardware attacks, TLS MitM, BTLE sniffing and App decompilation to show why those devices and their manufacturers aren't always that smart after all. And that even AES128 on top of the BTLE layer doesn't have to mean "unbreakable". Our main target will be electronic locks, but the methods shown apply to many other smart devices as well...
12/28/16
Hardware & Making
Xobs
Saal G
How to get USB running on an ARM microcontroller that has no built in USB hardware. We'll cover electrical requirements, pin assignments, and microcontroller considerations, then move all the way up the stack to creating a bidirectional USB HID communications layer entirely in software.
12/28/16
Hardware & Making
Saal G
Refugees are dying in the Mediterranean Sea. Thousands of them. We are building fixed wing drones, autonomously searching for refugee-vessels in a radius of 50km around a base-ship. The association "Seawatch e.V." has bought two well equipped Ships to help and rescue those people. But to help them we first have to find them.