Digital Design Equivalence Checking
Logic circuit analysis and optimization
Certificate protocol 0.2.0 and standalone reference verifier for AlchemQ proof-carrying quantum circuit optimization. Optimization engine not included.
A Web-based tool that helps analyze the correctness and equivalence of programs using formal methods.
Behavior-first program synthesis engine that discovers compact implementations, collapses semantically equivalent programs, and exhaustively verifies behavior across bounded input domains.
Small parallel RTL compiler in C++: Verilog/SystemVerilog subset to optimized gate-level netlist, with region-parallel optimization on a work-stealing pool
Formal verification of Minecraft redstone circuits: SAT + LRAT certificates, Lean 4 proofs, Verilog equivalence checking, vanilla-game oracle
Context-verified, error-budget-aware decomposition selection for Toffoli networks. Companion code to arXiv:2606.31791 (Bartkiewicz & Tulewicz, submitted to Quantum).
Portable, independently re-derivable logic-equivalence receipts — DRAT checking with zero dependencies
Bounded equivalence checker that proves an AI-refactored function matches the original, or finds a counterexample. Uses differential testing and Z3 symbolic execution.
Sequential radix-2 Booth multiplier with three sign-handling architectures, each with an exactly predicted set of failing operands, confirmed by exhaustive simulation of all 2^26 pairs and by unbounded proofs and counterexamples (Yosys + ABC PDR). Includes a SAT equivalence-checking demo.
Lean formalization of how behavioral equivalence checking can be generalized through abstract intrepretation
Combinational logic equivalence check: two gate-level netlists in, an equivalence verdict (with counter-example) out.
Research prototype for automated equivalence checking of hybrid quantum circuits.
To associate your repository with the equivalence-checking topic, visit your repo's landing page and select "manage topics."