Formal Verification

[andrewb1999]

SymbiFlow Formal Verification

Next semester I am doing an independent study on formal verification and am planning on doing a project involving SymbiFlow. My initial thought is performing formal equivalence checking between post-synthesis verilog and the verilog output of fasm2bels. I think this could provide an interesting way for verifying that placement and routing produced reasonable results without having to go back into Vivado.

Would a system like this be useful in the SymbiFlow ecosystem and CI?

I'm also open to other ideas related to formal verification if anyone has one.

[mithro]

FYI - There is a bunch of documentation in SymbiFlow Checking / Testing Approach.

This image should be particularly useful;

I believe we have some formal verification of things like counters but I'm unsure what the status is.

[umarcor]

FTR, the state of formal verification using the Property Specification Language (PSL), included in VHDL 2008, and supported by GHDL + Yosys + Symbiyosys: ghdl/ghdl#1616. See also:

• https://github.com/tmeissner/formal_hw_verification
• https://github.com/tmeissner/psl_with_ghdl

In tmeissner/formal_hw_verification, CI is done with containers from hdl/containers (see docs). In fact, recently, @tmeissner helped adding several solvers.

@andrewb1999, feel free to discuss whether the images available in hdl/containers are useful to you, and/or which tools are missing.

GitHub

tmeissner/formal_hw_verification

Trying to verify Verilog/VHDL designs with formal methods and tools - tmeissner/formal_hw_verification

GitHub

tmeissner/psl_with_ghdl

Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys) - tmeissner/psl_with_ghdl