SMART EDA EMPOWERMENT
ON-SITE & ONLINE TRAINING
01 / APPROACHABLE
Get to know the basic concepts of Formal Verification using both the Open Source Yosys formal verification tool suite and our commercial-grade Symbiotic EDA Suite.
02 / HANDS-ON
Our 16 hours course covers not only the basic formal verification properties, such as assume and assert, but also the more advanced operators used to frame them, $past, $rase, $global_clock, etc.
03 / EMPOWERED
You will examine several real-world examples during the course. These include basic counters, a serial peripheral interface (SPI) port, as well as the formal properties necessary for a bus interface.
INTRODUCTION TO FORMAL VERIFICATION
This two-day course will include how to use SymbiYosys and Yosys-SMTBMC in all of its primary modes. These include:
Bounded Model Checking (BMC) Mode
Proves that a design meets its formal properties during the first N clock cycles.
Uslng K-lnductlon or more advanced methods, it is possible to prove that the formal properties hold for all clock cycles.
Proves not only, that the design can enter into a given state, but also reveals a path of how it might get there.
The final lesson will discuss the SystemVerilog Assertions (SVA) properties, and how they can be used to express many things at once.
Students will be required to bring a laptop with them that has gtkwave, ssh and scp. This laptop can be Windows, Mac, Linux, etc. lt will be used to connect to, and interact with, a server where the formal verification tools will be installed.
The majority of this course will demonstrate how to use formal methods using the open source Yosys tool suite. The last portion of the course, however, will use the commercial variant of Yosys. This commercial variant also provides VHDL and SystemVerilog support.
Attendees should have both a working knowledge of Verilog, as well as a basic knowledge of the Linux command line tools.
Students will learn how to:
Use formal properties to find faults within their code
Recognize and address common problems when using formal methods
Write successful formal properties for common RTL problems
Create the formal properties for a bus structure
Use formal properties to verify a bridge between two types of buses
The course will consist of alternating sections of lectures and labs. The labs will range from examining a simple counter, to demonstrating common difficulties when using formal methods, to ultimately creating the formal properties necessary to verify a bridge between two buses.
Dan Gisselquist ls an experienced digital designer who has recently learned how to use formal verification as a debugging tool. As a recent beginner in formal verification methods, he comes to the task with fresh experiences and plenty of examples of how he has used formal methods to find faults in his own designs, designs that he had thought were bug-free.