From adce21a91f4b55cad1126fa4d453b4d6eef79f7f Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Wed, 24 Jun 2026 07:58:06 +0000 Subject: Add CI pipeline for formal verification * Add formal verification tests with sby to CI * Fix reviewdog having insufficient API permissions See-also: #15 Signed-off-by: Warrick Lo --- dv/formal/regfile/regfile.sby | 26 ++++ dv/formal/regfile/regfile_fv.sv | 248 ++++++++++++++++++++++++++++++ dv/formal/simple_alu/README.md | 23 +++ dv/formal/simple_alu/simple_alu.sby | 22 +++ dv/formal/simple_alu/simple_alu_bind.sv | 15 ++ dv/formal/simple_alu/simple_alu_fv.sv | 50 ++++++ dv/formal/simple_alu/simple_alu_top_fv.sv | 37 +++++ dv/tb/rv32e_model.py | 5 + dv/tb/test.sv | 0 dv/uvm/env.sv | 0 10 files changed, 426 insertions(+) create mode 100644 dv/formal/regfile/regfile.sby create mode 100644 dv/formal/regfile/regfile_fv.sv create mode 100644 dv/formal/simple_alu/README.md create mode 100644 dv/formal/simple_alu/simple_alu.sby create mode 100644 dv/formal/simple_alu/simple_alu_bind.sv create mode 100644 dv/formal/simple_alu/simple_alu_fv.sv create mode 100644 dv/formal/simple_alu/simple_alu_top_fv.sv create mode 100644 dv/tb/rv32e_model.py create mode 100644 dv/tb/test.sv create mode 100644 dv/uvm/env.sv (limited to 'dv') diff --git a/dv/formal/regfile/regfile.sby b/dv/formal/regfile/regfile.sby new file mode 100644 index 0000000..a976a29 --- /dev/null +++ b/dv/formal/regfile/regfile.sby @@ -0,0 +1,26 @@ +[tasks] +cover +bmc +prove + +[options] +cover: mode cover +bmc: mode bmc +bmc: depth 50 +prove: mode prove +prove: depth 20 + +[engines] +smtbmc + +[script] +read -formal -sv config_pkg.sv +read -formal -sv regfile.sv +read -formal -sv regfile_fv.sv +prep -top regfile_fv + +[files] +rtl/types.svh +rtl/config_pkg.sv +rtl/regfile.sv +dv/formal/regfile/regfile_fv.sv diff --git a/dv/formal/regfile/regfile_fv.sv b/dv/formal/regfile/regfile_fv.sv new file mode 100644 index 0000000..795024e --- /dev/null +++ b/dv/formal/regfile/regfile_fv.sv @@ -0,0 +1,248 @@ +/* SPDX-License-Identifier: CERN-OHL-P-2.0 */ + +/* + * Copyright 2026 UBC ASIC contributors (Montreal project). + * + * Author: Warrick Lo + * + * Formal verification of regfile requirements + * + * This module verifies the regfile module against the requirements + * specified in the design specification. + * + * The following parameters are used for all tests: + * - Word width: 32 bits wide + * - Slice width: 8 bits wide + * - Number of words: 16 words + * - Number of read ports: 2 + * + * The following are design requirements that are assumed to be verifed by construction: + * - REQ-REGFILE-010 + * - REQ-REGFILE-040 + * REQ-REGFILE-010 is further verified below. + * + * The following requirements are verified through this module: + * - Cover: + * - REQ-REGFILE-053 + * - Bounded model checking: + * - REQ-REGFILE-010 + * - REQ-REGFILE-053 + * - K-induction: + * - REQ-REGFILE-020 + * - REQ-REGFILE-030 + * - REQ-REGFILE-041 + * - REQ-REGFILE-042 + * - REQ-REGFILE-043 + * - REQ-REGFILE-050 + * - REQ-REGFILE-051 + * - REQ-REGFILE-052 + * - REQ-REGFILE-060 + * + * See also: MAS, Regfile Specification, version 0.2 + * rtl/regfile.sv + */ + +`include "types.svh" + +module regfile_fv ( + input logic clk_i, + input logic rst_ni, + input logic [1:0] slice_sel_i, + + input logic [1:0][3:0] raddr_i, + + input logic wen_i, + input logic [3:0] waddr_i, + input logic [7:0] wdata_i +); + + /* + * DUT interface and internal signals. + */ + + word_bank_t register; + logic [1:0][7:0] rdata; + + /* + * DUT instance. + */ + + regfile #( + .XLEN(32), + .SLICE_WIDTH(8), + .ADDR_WIDTH(4), + .NUM_READ_PORTS(2) + ) dut ( + .register_dbg(register), + .clk_i, + .rst_ni, + .slice_sel_i, + + .raddr_i, + .rdata_o(rdata), + + .wen_i, + .waddr_i, + .wdata_i + ); + + /* + * Some assertions use $past(), which requires at least one clock edge. + * Those tests will use past_valid to check if a valid history exists. + */ + + logic past_valid; + + initial assume (past_valid == '0); + + always_ff @(posedge clk_i) begin : past_valid_dff + /* verilog_lint: waive dff-name-style */ + past_valid <= '1; + end : past_valid_dff + + /* + * REQ-REGFILE-010: + * The module must store NUM_WORDS words, each XLEN bits wide. + */ + + /* The definition of 'register' must use the type defined in types.svh. */ + initial assert ($bits(register) == 16 * 32); + + /* + * REQ-REGFILE-020: + * Slice k of word n shall correspond to bits [(k+1)*SLICE_WIDTH−1:k*SLICE_WIDTH] + * of register n, partitioning each word into XLEN/SLICE_WIDTH + * non-overlapping slices, each SLICE_WIDTH bits wide. + * + * REQ-REGFILE-050: + * The read output rdata_o[i] shall be combinationally derived from + * the current register state, raddr_i[i], and slice_sel_i. There shall not + * be any latency on reads. + * + * REQ-REGFILE-051: + * The read output rdata_o[i] must reflect the slice selected by slice_sel_i + * within the register selected by raddr_i[i]. + * + * Note: These three requirements are easiest to verify together. + */ + + /* We explicitly ignore the use of part-selects to verify the description of REQ-REGFILE-020. */ + always_comb begin : req_020_050_051 + if (raddr_i[0] != '0) begin + assert (rdata[0] == register[raddr_i[0]][(slice_sel_i + 1) * 8 - 1 : slice_sel_i * 8]); + end + if (raddr_i[1] != '0) begin + assert (rdata[1] == register[raddr_i[1]][(slice_sel_i + 1) * 8 - 1 : slice_sel_i * 8]); + end + end : req_020_050_051 + + /* + * REQ-REGFILE-030: + * Register contents must be 0 at most one clock after the synchronous reset is asserted. + */ + + always_ff @(posedge clk_i) begin : req_030 + if (past_valid && $past(!rst_ni, 1)) begin + assert (register == '0); + end + end : req_030 + + /* + * REQ-REGFILE-041: + * Writes to the register file must only occur when wen_i is asserted. + */ + + always_ff @(posedge clk_i) begin : req_041 + if (past_valid && $past(rst_ni && !wen_i, 1)) begin + /* Satisfies the requirement, but possibly not the intended RTL behaviour. + * See ticket #14. */ + assert ($stable(register)); + end + end : req_041 + + /* + * REQ-REGFILE-042: + * Contents of wdata_i must be written only to the slice selected by slice_sel_i + * within the register selected by waddr_i. All other slices of the target register + * shall remain unchanged. + */ + + /* We'll use a part-select to obtain the slice data since we can assume that + * slice_sel_i will select the correct slice within the target register, + * according to requirement REQ-REGFILE-020. */ + always_ff @(posedge clk_i) begin : req_042 + /* For register 0, this test will specifically permit writes targeting + * the register to succeed. The stability of register 0 is separately + * verified below in REQ-REGFILE-043. */ + for (int i = 0; i < 16; i++) begin : word_loop + for (int j = 0; j < 4; j++) begin : slice_loop + /* Ignore reset events. */ + if (past_valid && $past(rst_ni, 1)) begin + if ($past((waddr_i == i) && (slice_sel_i == j), 1)) begin + assert ($stable(register[i][j*8+:8]) || (register[i][j*8+:8] == $past(wdata_i, 1))); + end else begin + assert ($stable(register[i][j*8+:8])); + end + end + end : slice_loop + end : word_loop + end : req_042 + + /* + * REQ-REGFILE-043: + * Writes to register 0 shall be silently ignored, regardless of the state of wen_i. + */ + + always_ff @(posedge clk_i) begin : req_043 + if (past_valid && $past(rst_ni && (waddr_i == '0), 1)) begin + assert ($stable(register[0])); + end + end : req_043 + + /* + * REQ-REGFILE-052: + * The read output rdata[i] must be zero when raddr[i] is zero, + * regardless of any prior writes to register 0. + */ + + always_comb begin : req_052 + if (raddr_i[0] == '0) assert (rdata[0] == '0); + if (raddr_i[1] == '0) assert (rdata[1] == '0); + end : req_052 + + /* + * REQ-REGFILE-053: + * Requirement REQ-REGFILE-052 shall be unconditional: it must hold at power-on + * without reset having been asserted, and at all times during normal operation. + */ + + logic rst_asserted; + + initial assume (rst_asserted == '0); + + always_ff @(posedge clk_i) begin : req_053 + if (!rst_ni) begin + rst_asserted <= '1; + end + + cover (!rst_asserted && wen_i && (waddr_i == '0)); + end : req_053 + + /* + * REQ-REGFILE-060: + * The module shall not implement any bypass logic. A read and write to + * the same address in the same cycle shall return the value held in + * the register prior to the rising clock edge of the current cycle. + */ + + /* Similar to above, we will use a part-select here. */ + always_comb begin : req_060 + if (wen_i && raddr_i[0] != '0 && raddr_i[0] == waddr_i) begin + assert (rdata[0] == register[raddr_i[0]][slice_sel_i*8+:8]); + end + if (wen_i && raddr_i[1] != '0 && raddr_i[1] == waddr_i) begin + assert (rdata[1] == register[raddr_i[1]][slice_sel_i*8+:8]); + end + end : req_060 + +endmodule : regfile_fv diff --git a/dv/formal/simple_alu/README.md b/dv/formal/simple_alu/README.md new file mode 100644 index 0000000..3355ced --- /dev/null +++ b/dv/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/dv/formal/simple_alu/simple_alu.sby b/dv/formal/simple_alu/simple_alu.sby new file mode 100644 index 0000000..4f4f3cd --- /dev/null +++ b/dv/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 +dv/formal/simple_alu/simple_alu_fv.sv +dv/formal/simple_alu/simple_alu_top_fv.sv diff --git a/dv/formal/simple_alu/simple_alu_bind.sv b/dv/formal/simple_alu/simple_alu_bind.sv new file mode 100644 index 0000000..8ed7057 --- /dev/null +++ b/dv/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) +); diff --git a/dv/formal/simple_alu/simple_alu_fv.sv b/dv/formal/simple_alu/simple_alu_fv.sv new file mode 100644 index 0000000..98c05a7 --- /dev/null +++ b/dv/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/dv/formal/simple_alu/simple_alu_top_fv.sv b/dv/formal/simple_alu/simple_alu_top_fv.sv new file mode 100644 index 0000000..8f1241c --- /dev/null +++ b/dv/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/dv/tb/rv32e_model.py b/dv/tb/rv32e_model.py new file mode 100644 index 0000000..eda163e --- /dev/null +++ b/dv/tb/rv32e_model.py @@ -0,0 +1,5 @@ +#Golden Reference model for RV32E Processor + +#Constants + +XLEN = 32 \ No newline at end of file diff --git a/dv/tb/test.sv b/dv/tb/test.sv new file mode 100644 index 0000000..e69de29 diff --git a/dv/uvm/env.sv b/dv/uvm/env.sv new file mode 100644 index 0000000..e69de29 -- cgit v1.2.3