From adce21a91f4b55cad1126fa4d453b4d6eef79f7f Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Wed, 24 Jun 2026 07:58:06 +0000 Subject: Add CI pipeline for formal verification * Add formal verification tests with sby to CI * Fix reviewdog having insufficient API permissions See-also: #15 Signed-off-by: Warrick Lo --- dv/formal/simple_alu/README.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 dv/formal/simple_alu/README.md (limited to 'dv/formal/simple_alu/README.md') diff --git a/dv/formal/simple_alu/README.md b/dv/formal/simple_alu/README.md new file mode 100644 index 0000000..3355ced --- /dev/null +++ b/dv/formal/simple_alu/README.md @@ -0,0 +1,23 @@ +# simple_alu Formal Verification + +Run with: `sby -f simple_alu.sby` from this directory. + +Reference: https://yosyshq.readthedocs.io/projects/sby/en/latest/reference.html + +## Mode + +Bounded Model Check (BMC, depth=100): proves assertions hold for the first 100 clock cycles. +A counterexample waveform is generated on failure. + +Prove mode (k-induction): proves assertions hold for infinite time. Much stronger guarantee but harder to converge. Change `mode bmc` to `mode prove` in the `.sby` to use it. + +## Properties + +| Name | Status | Description | +|-------------------|-------------|------------------------------------------| +| `a_rst_check` | implemented | y == 0 one cycle after reset asserts | +| `a_rst_overflow` | planned | overflow == 0 one cycle after reset | +| `a_add` | planned | y == a+b one cycle after sel=0 | +| `a_sub` | planned | y == a-b one cycle after sel=1 | +| `a_overflow_add` | planned | overflow correct for addition | +| `a_overflow_sub` | planned | overflow correct for subtraction | \ No newline at end of file -- cgit v1.2.3