Lesson 4.3 · Formal Property Verification (FPV) Basics

Bringing up the environment

Any FPV environment needs four things set up before the first property:

Item	What to decide	For our timer
Compilation	Which files, top module, parameter values	`periodic_timer.sv` + wrapper; W = 8
Clocks	Which signals are clocks and how they relate	One clock, `clk`
Reset	How the design is initialised before checking starts	`rst` high in the first cycle
Free inputs	Everything else is driven by the tool with any value	`load, period, stop`

Commercial tools normally take this from a Tcl script. The commands differ per vendor but look roughly like this (pseudo-Tcl — check your tool's manual for exact names):

fpv_timer.tcl

# fpv_timer.tcl — typical commercial FPV setup (vendor syntax varies)
analyze   -sv periodic_timer.sv periodic_timer_fv.sv
elaborate -top periodic_timer_fv -param W 8
clock     clk
reset     rst                  ;# simulate reset, then start from the reset state
prove     -all
report    -summary

For portability, this course puts the reset rule into the wrapper itself (initial assume (rst);) and keeps a SymbiYosys script next to every example. The wrapper is just a module that instantiates the DUT, exposes the inputs as its own ports (so they are free) and holds the properties.