conceptintermediateconfidence 5/5CC BY 4.0

Formal verification: minimal explanation

Formal verification proves properties over all possible inputs within a bounded or inductive model instead of checking selected simulation traces.

Formal is strongest when the property is small, precise and tied to a real invariant: FIFOs do not underflow, counters stay in range, bus acknowledgements follow requests. Start with one module and one property.

Graph links

Boards: icebreaker/icebreaker
Chips: none
Toolchains: symbiyosys, yosys
Protocols: fifo, axi, wishbone
Pitfalls: A proof of the wrong property is still wrong. Unconstrained inputs can make proofs meaningless.

Commands

sby -f proof.sby

Related boards

iCEBreaker FPGAiCE40 UltraPlusbeginnerconfidence 4/5
iCEBreaker

Open-source educational Lattice iCE40UP5K board designed around the Yosys, nextpnr and IceStorm flow.

iCE40UP5K-SG48open toolchainprice unknowneducationcontroldspformal

Sources

Suggest correction