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
---
 .gitignore | 5 +++++
 1 file changed, 5 insertions(+)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 59a8a35..ad3001c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,8 @@
 *.swo
 .vscode
 .claude/
+
+# SymbiYosys output
+verif/formal/simple_alu/simple_alu/
+verif/formal/simple_alu/simple_alu_bmc/
+verif/formal/simple_alu/simple_alu_cover/
-- 
cgit v1.2.3