I teach the course, An Introduction to Formal Methods, on behalf of SymbioticEDA. The course features their Symbiotic EDA Suite of programs, centered around a commercial version of SymbiYosys. This program can be used to formally verify FPGA or ASIC components to verify functionality, and builds off of the functionality found in the open source version of SymbiYosys.

Feel free to review the slides and exercises I use when teaching the course below.

  • Verilog slides

    Although the Symbiotic EDA Suite can handle SystemVerilog with all of its features, I’ve chosen in the course to stick closer to the original Verilog subset of System Verilog just to keep the course as broadly applicable to as many students as possible.

  • VHDL slides

    The Symbiotic EDA Suite also has full support for VHDL. Formal verification when using VHDL is done with SystemVerilog properties, either bound to the file of interest or as a wrapper around it. This VHDL version of the course therefore focuses on VHDL examples with SystemVerilog files containing formal properties.

  • Class exercises (both VHDL and Verilog): TGZ, ZIP

Some of the big things I provide, as an instructor and separate from the slides above, are 1) individual one-on-one attention on student exercises, helping to guarantee every student succeeds, 2) answers to student questions and concerns about how to make formal verification work in their environment, 3) stories and examples of what has worked well (or not) for me, together with any lessons learned from these projects, and even to some extent 4) examples of formal verification being used in more commercial projects as time and opportunity permit.

The course is offered either on-line or in-person and on-site. The format and the cost of the two offerings are subtly different.

  • On-line

    I teach the course on line using the Zoom teleconferencing application. When taught on-line, the course is structured as four 4-hr days of lessons. I offer this course for $1200 for the first person, and $1800 for two people.

    Matt Venn also teaches this course on line as well, and often for a slightly lower price. Feel free to schedule with either of us if you are interested.

  • On-site

    I also teach the course on-site as a two-day hands on course for up to six individuals at once. In this case, the course costs $4k plus whatever my travel costs might be.

Either way you choose to take the course, it comes with an evaluation license of the Symbiotic EDA Suite–providing access to not only VHDL and System Verilog, but also to the full System Verilog Assertion language.

The course is not designed for beginning HDL designers, but rather for those who already have some design experience and even use it in their day to day job. If you are a beginning designer, feel free to examine by beginner’s tutorial instead.

If you are at all interested in taking this course, please send me an e-mail and we can arrange a time that will meet your need.