Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Formal Verification #60

Open
andrewb1999 opened this issue Dec 23, 2020 · 2 comments
Open

Formal Verification #60

andrewb1999 opened this issue Dec 23, 2020 · 2 comments

Comments

@andrewb1999
Copy link

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
Copy link
Contributor

mithro commented Dec 23, 2020

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
Copy link

umarcor commented Jan 20, 2021 •
edited by unfurl-links bot

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
Trying to verify Verilog/VHDL designs with formal methods and tools - tmeissner/formal_hw_verification
GitHub
Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys) - tmeissner/psl_with_ghdl

@kgugala kgugala changed the title SymbiFlow Formal Verification Formal Verification Feb 18, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@mithro @andrewb1999 @umarcor