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 --- .github/workflows/format.yaml | 11 +- .github/workflows/lint.yaml | 16 +- .github/workflows/test.yaml | 22 +++ 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 tb/rv32e_model.py | 5 - tb/test.sv | 0 verif/formal/regfile/regfile.sby | 23 --- verif/formal/regfile/regfile_fv.sv | 248 --------------------------- verif/formal/simple_alu/README.md | 23 --- verif/formal/simple_alu/simple_alu.sby | 22 --- verif/formal/simple_alu/simple_alu_bind.sv | 15 -- verif/formal/simple_alu/simple_alu_fv.sv | 50 ------ verif/formal/simple_alu/simple_alu_top_fv.sv | 37 ---- verif/uvm/env.sv | 0 23 files changed, 463 insertions(+), 435 deletions(-) create mode 100644 .github/workflows/test.yaml 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 delete mode 100644 tb/rv32e_model.py delete mode 100644 tb/test.sv delete mode 100644 verif/formal/regfile/regfile.sby delete mode 100644 verif/formal/regfile/regfile_fv.sv delete mode 100644 verif/formal/simple_alu/README.md delete mode 100644 verif/formal/simple_alu/simple_alu.sby delete mode 100644 verif/formal/simple_alu/simple_alu_bind.sv delete mode 100644 verif/formal/simple_alu/simple_alu_fv.sv delete mode 100644 verif/formal/simple_alu/simple_alu_top_fv.sv delete mode 100644 verif/uvm/env.sv diff --git a/.github/workflows/format.yaml b/.github/workflows/format.yaml index fbef4a8..1c32511 100644 --- a/.github/workflows/format.yaml +++ b/.github/workflows/format.yaml @@ -5,8 +5,11 @@ on: [pull_request] jobs: format: runs-on: ubuntu-latest + permissions: + contents: read + pull-requests: write steps: - - uses: actions/checkout@master - - uses: chipsalliance/verible-formatter-action@main - with: - github_token: ${{ secrets.GITHUB_TOKEN }} + - uses: actions/checkout@master + - uses: chipsalliance/verible-formatter-action@main + with: + github_token: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/lint.yaml b/.github/workflows/lint.yaml index 94ad728..91424ca 100644 --- a/.github/workflows/lint.yaml +++ b/.github/workflows/lint.yaml @@ -6,11 +6,11 @@ jobs: lint: runs-on: ubuntu-latest steps: - - uses: actions/checkout@master - - uses: chipsalliance/verible-linter-action@main - with: - config_file: "lint.rules" - github_token: ${{ secrets.GITHUB_TOKEN }} - - name: Fail on lint errors - run: | - verible-verilog-lint --lint_fatal=true --rules_config=lint.rules $(find . -name "*.sv" -o -name "*.v") + - uses: actions/checkout@master + - uses: chipsalliance/verible-linter-action@main + with: + config_file: "lint.rules" + github_token: ${{ secrets.GITHUB_TOKEN }} + - name: Fail on lint errors + run: | + verible-verilog-lint --lint_fatal=true --rules_config=lint.rules $(find . -name "*.sv" -o -name "*.v") diff --git a/.github/workflows/test.yaml b/.github/workflows/test.yaml new file mode 100644 index 0000000..ee45561 --- /dev/null +++ b/.github/workflows/test.yaml @@ -0,0 +1,22 @@ +name: Test + +on: [push, pull_request] + +jobs: + formal: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@master + - uses: YosysHQ/setup-oss-cad-suite@v4 + - name: Run test + shell: bash + run: | + sby -f dv/formal/regfile/regfile.sby + - name: Upload artifacts + uses: actions/upload-artifact@v7 + with: + name: formal-verification + path: | + dv/formal/regfile/regfile_bmc/* + dv/formal/regfile/regfile_cover/* + dv/formal/regfile/regfile_prove/* 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 diff --git a/tb/rv32e_model.py b/tb/rv32e_model.py deleted file mode 100644 index eda163e..0000000 --- a/tb/rv32e_model.py +++ /dev/null @@ -1,5 +0,0 @@ -#Golden Reference model for RV32E Processor - -#Constants - -XLEN = 32 \ No newline at end of file diff --git a/tb/test.sv b/tb/test.sv deleted file mode 100644 index e69de29..0000000 diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby deleted file mode 100644 index 69cb7b9..0000000 --- a/verif/formal/regfile/regfile.sby +++ /dev/null @@ -1,23 +0,0 @@ -[tasks] -cover -prove - -[options] -cover: mode cover -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 -verif/formal/regfile/regfile_fv.sv diff --git a/verif/formal/regfile/regfile_fv.sv b/verif/formal/regfile/regfile_fv.sv deleted file mode 100644 index 795024e..0000000 --- a/verif/formal/regfile/regfile_fv.sv +++ /dev/null @@ -1,248 +0,0 @@ -/* 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/verif/formal/simple_alu/README.md b/verif/formal/simple_alu/README.md deleted file mode 100644 index 3355ced..0000000 --- a/verif/formal/simple_alu/README.md +++ /dev/null @@ -1,23 +0,0 @@ -# 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 deleted file mode 100644 index cd028d9..0000000 --- a/verif/formal/simple_alu/simple_alu.sby +++ /dev/null @@ -1,22 +0,0 @@ -[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 deleted file mode 100644 index 8ed7057..0000000 --- a/verif/formal/simple_alu/simple_alu_bind.sv +++ /dev/null @@ -1,15 +0,0 @@ -// 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/verif/formal/simple_alu/simple_alu_fv.sv b/verif/formal/simple_alu/simple_alu_fv.sv deleted file mode 100644 index 98c05a7..0000000 --- a/verif/formal/simple_alu/simple_alu_fv.sv +++ /dev/null @@ -1,50 +0,0 @@ -// 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 deleted file mode 100644 index 8f1241c..0000000 --- a/verif/formal/simple_alu/simple_alu_top_fv.sv +++ /dev/null @@ -1,37 +0,0 @@ -// 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 deleted file mode 100644 index e69de29..0000000 -- cgit v1.2.3 From 70d49a69e4b729806aa5255f091981206dc9e662 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Fri, 26 Jun 2026 10:50:59 +0000 Subject: Add DCO [skip ci] Signed-off-by: Warrick Lo --- DCO | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 DCO diff --git a/DCO b/DCO new file mode 100644 index 0000000..49b8cb0 --- /dev/null +++ b/DCO @@ -0,0 +1,34 @@ +Developer Certificate of Origin +Version 1.1 + +Copyright (C) 2004, 2006 The Linux Foundation and its contributors. + +Everyone is permitted to copy and distribute verbatim copies of this +license document, but changing it is not allowed. + + +Developer's Certificate of Origin 1.1 + +By making a contribution to this project, I certify that: + +(a) The contribution was created in whole or in part by me and I + have the right to submit it under the open source license + indicated in the file; or + +(b) The contribution is based upon previous work that, to the best + of my knowledge, is covered under an appropriate open source + license and I have the right under that license to submit that + work with modifications, whether created in whole or in part + by me, under the same open source license (unless I am + permitted to submit under a different license), as indicated + in the file; or + +(c) The contribution was provided directly to me by some other + person who certified (a), (b) or (c) and I have not modified + it. + +(d) I understand and agree that this project and the contribution + are public and that a record of the contribution (including all + personal information I submit with it, including my sign-off) is + maintained indefinitely and may be redistributed consistent with + this project or the open source license(s) involved. -- cgit v1.2.3