diff options
| -rw-r--r-- | .gitignore | 5 | ||||
| -rw-r--r-- | rtl/regfile.sv | 0 | ||||
| -rw-r--r-- | rtl/simple_alu.sv | 58 | ||||
| -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 | 50 | ||||
| -rw-r--r-- | verif/formal/simple_alu/simple_alu_top_fv.sv | 37 | ||||
| -rw-r--r-- | verif/uvm/env.sv | 0 |
9 files changed, 210 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..a5ae9e7 --- /dev/null +++ b/rtl/simple_alu.sv @@ -0,0 +1,58 @@ +// 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_i, + input logic [31:0] a_i, + input logic [31:0] b_i, + input logic sel_i, //sel = 0 -> ADD, sel = 1 -> SUB + input logic rst_ni, //active LOW sync reset + + //outputs + output logic [31:0] y_o, + output logic overflow_o +); + + logic [32:0] sum; + logic [32:0] diff; + logic [31:0] y_r; + logic overflow_r; + logic [31:0] y_next; + logic overflow_next; + + always_comb begin + sum = {1'b0, a_i} + {1'b0, b_i}; + diff = {1'b0, a_i} - {1'b0, b_i}; + + y_next = '0; + overflow_next = '0; + + if (rst_ni) begin + case (sel_i) + 0: begin + y_next = sum[31:0]; + overflow_next = sum[32]; + end + 1: begin + y_next = diff[31:0]; + overflow_next = diff[32]; + end + default: begin + y_next = '0; + overflow_next = '0; + end + endcase + end + end + + always_ff @(posedge clk_i) begin + y_r <= y_next; + overflow_r <= overflow_next; + end + + assign y_o = y_r; + assign overflow_o = overflow_r; + +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..8ed7057 --- /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) +); 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..98c05a7 --- /dev/null +++ b/verif/formal/simple_alu/simple_alu_fv.sv @@ -0,0 +1,50 @@ +// 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_i, + input logic [31:0] a_i, + input logic [31:0] b_i, + input logic sel_i, + input logic rst_ni, + + input logic [31:0] y_i, + input logic overflow_i + ); + + // ------------------------------------------------------------------------- + // Initial assumptions - constrain starting state so solver doesn't + // explore garbage initial register values + // ------------------------------------------------------------------------- + initial assume (~rst_ni); + initial assume (y_i == '0); + initial assume (overflow_i == 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_i) + // ~rst_ni |=> (y_i=='0); + // endproperty + // a_rst_y: assert property (p_rst_y) + // else $error("RESET CHECK FAILED: rst_ni=%0b y_i=%0h, expected y=0", rst_ni, y_i); + + // Reset check - y must be 0 one cycle after reset asserts (active low) + always @(posedge clk_i) begin + if ($past(~rst_ni)) begin + assert (y_i == '0); + assert (overflow_i == 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_i) begin + cover ($past(sel_i == 0) && overflow_i == 1'b1); // addition overflow + cover ($past(sel_i == 1) && overflow_i == 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..8f1241c --- /dev/null +++ b/verif/formal/simple_alu/simple_alu_top_fv.sv @@ -0,0 +1,37 @@ +// 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_i, + input logic [31:0] a_i, + input logic [31:0] b_i, + input logic sel_i, + input logic rst_ni +); + logic [31:0] y; + logic overflow; + + // DUT instance + simple_alu dut ( + .clk_i (clk_i), + .a_i (a_i), + .b_i (b_i), + .sel_i (sel_i), + .rst_ni (rst_ni), + .y_o (y), + .overflow_o (overflow) + ); + + // Checker instance - observes DUT outputs + simple_alu_fv u_checker ( + .clk_i (clk_i), + .a_i (a_i), + .b_i (b_i), + .sel_i (sel_i), + .rst_ni (rst_ni), + .y_i (y), + .overflow_i (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 |