Formal Verification & PSL

31.1 Property Specification Language (PSL)

Integrated into VHDL-2008:

Assertions check behavior in simulation and are the input to formal tools.

-- psl default clock is rising_edge(clk);
-- psl assert always (req -> next_e[1 to 4](ack)) report "ack must follow req within 4 cycles";
-- psl assert never (full and wr_en);
-- psl cover {start; busy[*3]; done};
-- psl assume always (not (rd_en and empty));

31.2 Formal verification

Formal tools mathematically prove properties for all possible input sequences (within bounds):

Bounded model checking (BMC) — finds counterexamples up to N cycles.

k-induction / unbounded proofs — prove properties hold forever.

Cover checks — prove scenarios are reachable.

Tools: SymbiYosys (open source; with GHDL plugin for VHDL), Questa Formal, Cadence JasperGold, Synopsys VC Formal, OneSpin.

Also: equivalence checking (RTL vs netlist), linting (VSG, Sigasi, Blue Pearl, SpyGlass), CDC/RDC verification.

# fifo.sby (SymbiYosys)
[options]
mode prove
depth 20
[engines]
smtbmc
[script]
ghdl --std=08 sync_fifo.vhd -e sync_fifo
prep -top sync_fifo
[files]
sync_fifo.vhd