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.

• Full Proof

  • Uslng K-lnductlon or more advanced methods, it is possible to prove that the formal properties hold for all clock cycles.

• Cover

  • 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.

​

REQUIRED MATERIALS 

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.

​

PREREQUISITES

Attendees should have both a working knowledge of Verilog, as well as a basic knowledge of the Linux command line tools.

​

COURSE OBJECTIVES

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

​

COURSE STRUCTURE

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.

​