diff options
| -rw-r--r-- | .gitignore | 5 | ||||
| -rw-r--r-- | rtl/regfile.sv | 0 | ||||
| -rw-r--r-- | rtl/simple_alu.sv | 44 | ||||
| -rw-r--r-- | verif/formal/simple_alu/README.md | 23 | ||||
| -rw-r--r-- | verif/formal/simple_alu/simple_alu.sby | 22 | ||||
| -rw-r--r-- | verif/formal/simple_alu/simple_alu_bind.sv | 15 | ||||
| -rw-r--r-- | verif/formal/simple_alu/simple_alu_fv.sv | 51 | ||||
| -rw-r--r-- | verif/formal/simple_alu/simple_alu_top_fv.sv | 29 | ||||
| -rw-r--r-- | verif/uvm/env.sv | 0 |
9 files changed, 189 insertions, 0 deletions
@@ -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/ diff --git a/rtl/regfile.sv b/rtl/regfile.sv new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/rtl/regfile.sv diff --git a/rtl/simple_alu.sv b/rtl/simple_alu.sv new file mode 100644 index 0000000..8dc0586 --- /dev/null +++ b/rtl/simple_alu.sv @@ -0,0 +1,44 @@ +// Simple 32-bit ALU supporting addition and subtraction (sel=0/1). +// Outputs are registered. Overflow/underflow detected via 33-bit extended arithmetic. +// Active-low synchronous reset. Used as a sandbox for formal verification. +module simple_alu ( + + //inputs + input logic clk, + input logic [31:0] a, + input logic [31:0] b, + input logic sel, //sel = 0 -> ADD, sel = 1 -> SUB + input logic rst, //active LOW sync reset + + //outputs + output logic [31:0] y, + output logic overflow +); + + logic [32:0] sum; + logic [32:0] diff; + + always_comb begin + sum = {1'b0, a} + {1'b0, b}; + diff = {1'b0, a} - {1'b0, b}; + end + + always_ff @(posedge clk) begin + if (~rst) begin + y <= '0; + overflow <= '0; + end + else begin + case (sel) + 0: begin + y <= sum[31:0]; + overflow <= sum[32]; + end + 1: begin + y <= diff[31:0]; + overflow <= diff[32]; + end + endcase + end + end +endmodule 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 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 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 <dut_module> <fv_module> <instance_name> (<port_connections>); + +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 diff --git a/verif/formal/simple_alu/simple_alu_fv.sv b/verif/formal/simple_alu/simple_alu_fv.sv new file mode 100644 index 0000000..ea9700a --- /dev/null +++ b/verif/formal/simple_alu/simple_alu_fv.sv @@ -0,0 +1,51 @@ +// Formal verification module for simple_alu. +// All ports are inputs - this module only observes DUT signals, never drives them. +// Instantiated via simple_alu_top_fv.sv wrapper (bind unsupported in open-source Yosys). +module simple_alu_fv ( + input logic clk, + input logic [31:0] a, + input logic [31:0] b, + input logic sel, + input logic rst, + + input logic [31:0] y, + input logic overflow + ); + + // ------------------------------------------------------------------------- + // Initial assumptions - constrain starting state so solver doesn't + // explore garbage initial register values + // ------------------------------------------------------------------------- + initial assume(~rst); + initial assume(y == '0); + initial assume(overflow == 1'b0); + + //assertion check: if rst deasserted, y tied to 0 + //assertions are what we want to prove, formal verification is the engine that proves it + // property p_rst_y; + // @(posedge clk) + // ~rst |=> (y=='0); + // endproperty + // a_rst_y: assert property (p_rst_y) + // else $error("RESET CHECK FAILED: rst=%0b y=%0h, expected y=0", rst, y); + + // Reset check - y must be 0 one cycle after reset asserts (active low) + always @(posedge clk) begin + if ( $past(~rst)) begin + assert (y == '0); + assert (overflow == 0); + end + end + + // ------------------------------------------------------------------------- + // Cover statements - solver finds shortest path to reach each state + // These generate VCD traces you can inspect in GTKWave + // ------------------------------------------------------------------------- + + always @(posedge clk) begin + cover ($past(sel == 0) && overflow == 1'b1); // addition overflow + cover ($past(sel == 1) && overflow == 1'b1); // subtraction underflow + end + + +endmodule diff --git a/verif/formal/simple_alu/simple_alu_top_fv.sv b/verif/formal/simple_alu/simple_alu_top_fv.sv new file mode 100644 index 0000000..2292713 --- /dev/null +++ b/verif/formal/simple_alu/simple_alu_top_fv.sv @@ -0,0 +1,29 @@ +// Wrapper top module for formal verification of simple_alu. +// Instantiates the DUT and the checker side-by-side so the formal tool +// sees both. Used because open-source Yosys does not support bind. +// Note: only DUT ports are accessible here - internal signals (sum, diff) +// cannot be tapped without bind or Verific. +module simple_alu_top_fv ( + input logic clk, + input logic [31:0] a, + input logic [31:0] b, + input logic sel, + input logic rst +); + logic [31:0] y; + logic overflow; + + // DUT instance + simple_alu dut (.*); + + // Checker instance - observes DUT outputs + simple_alu_fv u_checker ( + .clk (clk), + .a (a), + .b (b), + .sel (sel), + .rst (rst), + .y (y), + .overflow (overflow) + ); +endmodule diff --git a/verif/uvm/env.sv b/verif/uvm/env.sv new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/verif/uvm/env.sv |