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/simple_alu_bind.sv | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 verif/formal/simple_alu/simple_alu_bind.sv (limited to 'verif/formal/simple_alu/simple_alu_bind.sv') diff --git a/verif/formal/simple_alu/simple_alu_bind.sv b/verif/formal/simple_alu/simple_alu_bind.sv new file mode 100644 index 0000000..b12e0eb --- /dev/null +++ b/verif/formal/simple_alu/simple_alu_bind.sv @@ -0,0 +1,15 @@ +// Bind file for simple_alu formal verification. +// Attaches simple_alu_fv to every instance of simple_alu in the design. +// RTL is completely unaware of this file. +// +// bind (); + +bind simple_alu simple_alu_fv u_simple_alu_fv ( + .clk (clk), + .rst (rst), + .a (a), + .b (b), + .sel (sel), + .y (y), + .overflow (overflow) +); \ No newline at end of file -- cgit v1.2.3