You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Formal verification reference flow: an FSM safety property proven unbounded by k-induction with SymbiYosys, Yosys, and z3. The same toolchain we use to prove coverage holes unreachable on real cores.
UVM 1.2 reference environment for a pipelined ALU: agent, driver, monitor, scoreboard with reference model, and functional coverage. Lints clean under Verilator.
Reusable SystemVerilog assertion (SVA) checkers for handshakes, FIFOs, one-hot buses, and CDC synchronizers. Bind into RTL for simulation or hand to a formal engine.
Python verification reference flow: cocotb 2.x testbench with a reference model, directed and constrained-random tests, and functional coverage. Verified on Icarus Verilog.
Clock-domain-crossing verification: a dual-clock asynchronous FIFO with Gray pointers and 2-flop synchronizers, checked across two independent clocks with cocotb. Verified on Icarus Verilog.