From 1fcb70209582fd05c03919b31502deb2b7af472a Mon Sep 17 00:00:00 2001
From: Chat <63841542+ChillZero@users.noreply.github.com>
Date: Thu, 14 May 2026 19:58:51 -0700
Subject: Add simple_alu RTL and formal verification

  - simple_alu.sv: 32-bit ALU with add/sub, 33-bit extended overflow
    detection, and active-low synchronous reset
  - simple_alu_bind.sv: attaches checker to simple_alu without modifying RTL
  - simple_alu_top_fv.sv: replace bind (unsupported in open-source Yosys)
    with explicit wrapper that instantiates DUT and checker side-by-side
  - simple_alu_fv.sv: bind-based checker module observing DUT signals
  - simple_alu.sby: SymbiYosys config running BMC and cover tasks
  - README.md: verification plan tracking implemented and planned properties
  - .gitignore: exclude SymbiYosys output directories
---
 verif/formal/simple_alu/README.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 verif/formal/simple_alu/README.md

(limited to 'verif/formal/simple_alu/README.md')

diff --git a/verif/formal/simple_alu/README.md b/verif/formal/simple_alu/README.md
new file mode 100644
index 0000000..3355ced
--- /dev/null
+++ b/verif/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