Introduction to Formal Verification with SymbiYosys
Description
Experience some of the benefits of formal verification with this hands on afternoon workshop. You will be introduced to the concept of formal verification, and learn the basics of how to use the open source tools to verify your designs.
Many engineers find formal tools too intimidating or expensive to use. The new open source tools developed by Symbiotic EDA are free to use and simple to start.
Formal tools greatly benefit the designer by providing additional assurance in the design and quickly discovering bugs that would be difficult to find with traditional simulation approaches.
In this short workshop, participants will:
- have gained hands on experience with the tools
- have used the tools to formally verify some simple designs
- have written their own formal properties to discover a bug in a computational pipeline
- have seen how bus properties can be used to validate an AXI-Lite peripheral.
Requirements
- Some experience of a HDL, ideally Verilog
- Computers will be provided, however you can install SymbiYosys and its dependencies in advance if you wish to use your own computer.
Outline
- What is Formal Verification and what is it useful for?
- How does it work? BMC and K Induction
- Overview of open source tools and a typical flow
- Basic assertions, assumptions and “cover”
- Getting started with the tools, verifying a simple counter
- Writing your own formal properties to find a bug in a computational pipeline
Organiser - David Shah
David is an engineer at Symbiotic EDA, working on open source design and verification tools including Yosys and nextpnr. He is the developer of the end-to-end open source “Trellis” flow for ECP5 FPGAs.
Questions? Email david@symbioticeda.com