diff options
| author | Warrick Lo <wlo@warricklo.net> | 2026-06-24 07:58:06 +0000 |
|---|---|---|
| committer | Warrick Lo <wlo@warricklo.net> | 2026-06-24 07:58:06 +0000 |
| commit | adce21a91f4b55cad1126fa4d453b4d6eef79f7f (patch) | |
| tree | 6132f55957a5e467cbb02e1eedecd4c75ff1e037 /verif/formal/simple_alu/README.md | |
| parent | Merge branch 'feature/core' (diff) | |
| download | montreal-adce21a91f4b55cad1126fa4d453b4d6eef79f7f.tar.xz montreal-adce21a91f4b55cad1126fa4d453b4d6eef79f7f.zip | |
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 <wlo@warricklo.net>
Diffstat (limited to 'verif/formal/simple_alu/README.md')
| -rw-r--r-- | verif/formal/simple_alu/README.md | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/verif/formal/simple_alu/README.md b/verif/formal/simple_alu/README.md deleted file mode 100644 index 3355ced..0000000 --- a/verif/formal/simple_alu/README.md +++ /dev/null @@ -1,23 +0,0 @@ -# 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 |