diff options
| author | Warrick Lo <wlo@warricklo.net> | 2026-07-07 06:01:17 +0000 |
|---|---|---|
| committer | Warrick Lo <wlo@warricklo.net> | 2026-07-07 06:01:17 +0000 |
| commit | 6c24f49f3239c79173fd180d065f8f03cfaeabfd (patch) | |
| tree | 4ac1ebc964784b655cda35de979331196b19a3c2 /verif/formal/simple_alu/README.md | |
| parent | Merge branch 'feature/fu' from MyDariell (diff) | |
| parent | Add DCO [skip ci] (diff) | |
| download | montreal-6c24f49f3239c79173fd180d065f8f03cfaeabfd.tar.xz montreal-6c24f49f3239c79173fd180d065f8f03cfaeabfd.zip | |
Sync with 'master'feature/fu
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 |