Build software better, together

tmeissner / psl_with_ghdl

Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)

vhdl assertions ghdl formal-verification yosys psl symbiyosys functional-coverage

Updated Feb 16, 2026
VHDL

A Dockerfile with a collections of ready to use open source EDA tools: Yosys, SimbiYosys (with Z3, boolector and Yices2), nextpnr-ice40, netxpnr-ecp5, nextpnr-gowin, Amaranth HDL, Silice and Verilator.

dockerfile eda z3 yosys verilator gowin boolector nmigen symbiyosys yices2 nextpnr-ice40 nextpnr-ecp5 amaranth silice openfpgaloader

Updated Jun 14, 2023
Dockerfile

tmeissner / formal_hw_verification

Star

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

vhdl verilog systemverilog ghdl formal-verification yosys psl symbiyosys

Updated Mar 7, 2024
VHDL

vmunoz82 / sudoku-challenge

Star

Solving Sudokus using open source formal verification tools

sudoku-solver sudoku formal-verification yosys symbiyosys

Updated Aug 16, 2022
Python

meiniKi / logIP

Star

Logic Analyzer IP Core

asic fpga digital amd ip verilog xilinx vivado ols systemverilog measurements hdl formal-verification basys3 hardware-description-language logicanalyzer sump logip symbiyosys

Updated Jul 23, 2022
SystemVerilog

agoessling / rules_symbiyosys

Star

Bazel rules for Symbiyosys.

fpga bazel bazel-rules verilog hdl formal-verification yosys symbiyosys rules-symbiyosys

Updated Nov 1, 2020
Starlark

que-ravon / fpga-tick-to-trade

Star

Deterministic, formally verified tick-to-trade engine in FPGA fabric — 5-cycle latency, zero CPU, proven fail-closed. SystemVerilog on Arty A7.

fpga trading low-latency ethernet systemverilog formal-verification cocotb symbiyosys hardware-design arty-a7

Updated Oct 22, 2026
SystemVerilog

kadirufukkandira / fpga-verification-demo

Star

FPGA verification demo using VHDL, VUnit, and SymbiYosys with GitHub Actions CI integration.

fpga vhdl ghdl formal-verification vunit github-actions-ci symbiyosys

Updated Jan 19, 2026
VHDL

fjpolo / Verilator_FormalVerification

Star

SymbiYosys (sby) Formal Verification

verification verilog formal-methods formal-verification verilog-hdl yosys wishbone verilator apb wishbone-bus amba-apb symbiyosys sby wishbone-master

Updated Feb 22, 2025
F#

billdmar / fifo-verification-suite

Star

8 SystemVerilog FIFO designs formally verified (SymbiYosys BMC + k-induction), mutation-tested, FPGA-characterized — green CI

fpga mutation-testing rtl systemverilog fifo cdc formal-verification yosys bmc verilator sva hardware-verification axi4-stream symbiyosys

Updated Aug 21, 2026
SystemVerilog

linuxuser314 / nano-rv32i

Star

This is where I am putting first RISC-V RV32I single-cycle processor (in development)

Updated Aug 4, 2026
SystemVerilog

rennelou / prettyosys

Star

Prettyosys is an easy-to-use and visually appealing wrapper for Symbioysys

fpga hardware vhdl verification rtl hardware-designs hdl formal-verification yosys symbiyosys

Updated Feb 3, 2023
Haskell

vsgautam22 / crc-engine

Star

Configurable CRC-8/16/32 hardware core — RTL, formal verification (SymbiYosys/Z3), Yosys synthesis, and SKY130A GDS tape-out

asic hardware rtl verilog crc vlsi formal-verification symbiyosys openlane sky130

Updated Mar 21, 2026
Verilog

taitashaw / cxl-type3-formal-signoff

Star

Formally verified vendor-neutral PCIe Gen5 / CXL Type-3 memory-expansion datapath. Unbounded k-induction safety proofs, two-clock CDC, and mutation-checked non-vacuity.

rtl systemverilog computer-architecture formal-verification pcie clock-domain-crossing hardware-verification design-verification symbiyosys cxl

Updated Aug 2, 2026
SystemVerilog

satchmakua / toroid

Star

An agent that reads a spec and RTL, proposes formal properties, runs a model checker, and iterates on counterexamples — automating the hardware verification engineer's loop.

eda rtl formal-verification ai-agents hardware-verification symbiyosys llm