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

1 files changed, 22 insertions, 0 deletions

diff --git a/verif/formal/simple_alu/simple_alu.sby b/verif/formal/simple_alu/simple_alu.sby
new file mode 100644
index 0000000..cd028d9
--- /dev/null
+++ b/verif/formal/simple_alu/simple_alu.sby
@@ -0,0 +1,22 @@
+[tasks]
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+depth 100
+
+[engines]
+smtbmc
+
+[script]
+read -formal -sv simple_alu.sv
+read -formal -sv simple_alu_fv.sv
+read -formal -sv simple_alu_top_fv.sv
+prep -top simple_alu_top_fv
+
+[files]
+../../../rtl/simple_alu.sv
+simple_alu_fv.sv
+simple_alu_top_fv.sv