search

f4pga / ideas

Random ideas and interesting ideas for things we hope to eventually do.
86 stars 9 forks source link

Formal Verification #60

Open andrewb1999 opened 3 years ago

andrewb1999 commented 3 years ago

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 commented 3 years ago

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

This image should be particularly useful; image

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

umarcor commented 3 years ago

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:

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