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 --- rtl/regfile.sv | 0 rtl/simple_alu.sv | 44 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 44 insertions(+) create mode 100644 rtl/regfile.sv create mode 100644 rtl/simple_alu.sv (limited to 'rtl') diff --git a/rtl/regfile.sv b/rtl/regfile.sv new file mode 100644 index 0000000..e69de29 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 -- cgit v1.2.3 From 429dd4fa609a5b8c71f8cd6ae6f8d74fd59f2280 Mon Sep 17 00:00:00 2001 From: Chat <63841542+chatrajaman3@users.noreply.github.com> Date: Tue, 19 May 2026 01:31:06 -0700 Subject: Pass linter - simple_alu.sv: rename ports with suffixes (clk_i, rst_ni, a_i, b_i, sel_i, y_o, overflow_o); add default case to sel case statement; add y_next and overflow_next combinational signals; simplify always_ff to only register y_next and overflow_next - simple_alu_fv.sv: rename ports to match RTL (clk_i, rst_ni, a_i, b_i, sel_i, y_i, overflow_i); remove trailing spaces - simple_alu_top_fv.sv: rename ports; replace .* with explicit connections to match updated port names - simple_alu_bind.sv: add missing posix newline at EOF --- rtl/simple_alu.sv | 64 +++++++++++++++++----------- verif/formal/simple_alu/simple_alu_bind.sv | 2 +- verif/formal/simple_alu/simple_alu_fv.sv | 45 ++++++++++--------- verif/formal/simple_alu/simple_alu_top_fv.sv | 34 +++++++++------ 4 files changed, 83 insertions(+), 62 deletions(-) (limited to 'rtl') diff --git a/rtl/simple_alu.sv b/rtl/simple_alu.sv index 8dc0586..a5ae9e7 100644 --- a/rtl/simple_alu.sv +++ b/rtl/simple_alu.sv @@ -4,41 +4,55 @@ 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 + 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, - output logic overflow + 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} + {1'b0, b}; - diff = {1'b0, a} - {1'b0, b}; - end + sum = {1'b0, a_i} + {1'b0, b_i}; + diff = {1'b0, a_i} - {1'b0, b_i}; - 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]; + 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 - endcase 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/simple_alu_bind.sv b/verif/formal/simple_alu/simple_alu_bind.sv index b12e0eb..8ed7057 100644 --- a/verif/formal/simple_alu/simple_alu_bind.sv +++ b/verif/formal/simple_alu/simple_alu_bind.sv @@ -12,4 +12,4 @@ bind simple_alu simple_alu_fv u_simple_alu_fv ( .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 index ea9700a..98c05a7 100644 --- a/verif/formal/simple_alu/simple_alu_fv.sv +++ b/verif/formal/simple_alu/simple_alu_fv.sv @@ -2,38 +2,38 @@ // 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 + 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); - initial assume(y == '0); - initial assume(overflow == 1'b0); + 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) - // ~rst |=> (y=='0); + // 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=%0b y=%0h, expected y=0", 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) begin - if ( $past(~rst)) begin - assert (y == '0); - assert (overflow == 0); + always @(posedge clk_i) begin + if ($past(~rst_ni)) begin + assert (y_i == '0); + assert (overflow_i == 0); end end @@ -42,10 +42,9 @@ module simple_alu_fv ( // 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 + 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 index 2292713..8f1241c 100644 --- a/verif/formal/simple_alu/simple_alu_top_fv.sv +++ b/verif/formal/simple_alu/simple_alu_top_fv.sv @@ -4,26 +4,34 @@ // 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 + 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 (.*); + 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 (clk), - .a (a), - .b (b), - .sel (sel), - .rst (rst), - .y (y), - .overflow (overflow) + .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 -- cgit v1.2.3 From 577ad51f728a56b1c2244cb21a563564e62999b6 Mon Sep 17 00:00:00 2001 From: Chat <63841542+chatrajaman3@users.noreply.github.com> Date: Sun, 14 Jun 2026 16:21:08 -0700 Subject: Add top-level and QSPI controller modules --- rtl/qspi_controller.sv | 38 +++++++++++++++++++++++++++++++ rtl/rv32e_core_wrapper.sv | 8 +++++++ rtl/tt_top.sv | 58 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 104 insertions(+) create mode 100644 rtl/qspi_controller.sv create mode 100644 rtl/rv32e_core_wrapper.sv create mode 100644 rtl/tt_top.sv (limited to 'rtl') diff --git a/rtl/qspi_controller.sv b/rtl/qspi_controller.sv new file mode 100644 index 0000000..15b3c96 --- /dev/null +++ b/rtl/qspi_controller.sv @@ -0,0 +1,38 @@ +// Interface between core and QSPI pmod +// https://onlinedocs.microchip.com/oxy/GUID-450989FA-38E4-4D68-AB61-15ADB29AD718-en-US-6/GUID-C2190631-B6F5-4CD7-B6DB-5267DC280E90_3.html + +module qspi_controller ( + // Clock + input wire clk, + + // Reset (active low) + input wire rst_n, + + // Bi-directional I/O + input wire [7:0] uio_in, // IOs: Input path + output wire [7:0] uio_out, // IOs: Output path + output wire [7:0] uio_oe, // IOs: Enable path (active high: 0=input, 1=output) +); + + // ==================================== + // Pin mapping + // ==================================== + + // QSPI Serial CLK + + // QSPI CS - Active Low + + // QSPI IO_0 + // QSPI IO_1 + // QSPI IO_2 + // QSPI IO_3 + + + logic qspi_clk; + logic qspi_cs_n; + logic [3:0] qspi_data; + + + + +endmodule diff --git a/rtl/rv32e_core_wrapper.sv b/rtl/rv32e_core_wrapper.sv new file mode 100644 index 0000000..8d2b5c9 --- /dev/null +++ b/rtl/rv32e_core_wrapper.sv @@ -0,0 +1,8 @@ +// Provides a clean, generic bus interface for the core +// Easier UVM access + +module rv32e_core_wrapper (); + + + +endmodule diff --git a/rtl/tt_top.sv b/rtl/tt_top.sv new file mode 100644 index 0000000..be5f40d --- /dev/null +++ b/rtl/tt_top.sv @@ -0,0 +1,58 @@ +/* + * Copyright (c) 2026 UBC ASIC + * SPDX-License-Identifier: Apache-2.0 + */ + +// Core wrapper + QSPI PMOD controller + +`default_nettype none + +module tt_top ( + // Dedicated inputs + input wire [7:0] ui_in, + + // Dedicated outputs + output wire [7:0] uo_out, + + // Bi-directional I/O + input wire [7:0] uio_in, // IOs: Input path + output wire [7:0] uio_out, // IOs: Output path + output wire [7:0] uio_oe, // IOs: Enable path (active high: 0=input, 1=output) + + // Enable design + input wire ena, // always 1 when the design is powered, so you can ignore it + + // Clock + input wire clk, // clock + + // Reset + input wire rst_n // reset_n - low to reset +); + + // All output pins must be assigned. If not used, assign to 0. + assign uo_out = ui_in + uio_in; // Example: ou_out is the sum of ui_in and uio_in + assign uio_out = 0; + assign uio_oe = 0; + + // List all unused inputs to prevent warnings + wire _unused = &{ena, clk, rst_n, 1'b0}; + + + u_rv32e_core_wrapper rv32e_core_wrapper( + + ); + + + u_qspi_controller qspi_controller( + // Clock + .clk(), + + // Reset + .rst_n(), + + // Bi-directional I/O + .uio_in(), // IOs: Input path + .uio_out(), // IOs: Output path + .uio_oe(), // IOs: Enable path (active high: 0=input, 1=output) + ); +endmodule -- cgit v1.2.3 From eef204455c692cee60e3713bad6c7428627b3672 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Sun, 14 Jun 2026 18:18:32 -0700 Subject: Rename top-level module to prevent clashes Also fixes linter errors, whitespace, and copyright. Top-level module name MUST be unique to avoid collisions with other projects in the shuttle run. The port list MUST also exactly follow the Tiny Tapeout template, so a comment has been added to emphasise this. Signed-off-by: Warrick Lo --- rtl/qspi_controller.sv | 77 +++++++++++++++++++--------------- rtl/rv32e_core_wrapper.sv | 18 +++++--- rtl/tt_top.sv | 105 ++++++++++++++++++++++++++-------------------- 3 files changed, 115 insertions(+), 85 deletions(-) (limited to 'rtl') diff --git a/rtl/qspi_controller.sv b/rtl/qspi_controller.sv index 15b3c96..e718b50 100644 --- a/rtl/qspi_controller.sv +++ b/rtl/qspi_controller.sv @@ -1,38 +1,47 @@ -// Interface between core and QSPI pmod -// https://onlinedocs.microchip.com/oxy/GUID-450989FA-38E4-4D68-AB61-15ADB29AD718-en-US-6/GUID-C2190631-B6F5-4CD7-B6DB-5267DC280E90_3.html - +/* SPDX-License-Identifier: CERN-OHL-P-2.0 */ + +/* + * Copyright 2026 UBC ASIC contributors (Montreal project). + * All rights reserved. + * + * Authors: Chathil Rajamanthree + * + * Interface between core and QSPI Pmod + * + * https://onlinedocs.microchip.com/oxy/GUID-450989FA-38E4-4D68-AB61-15ADB29AD718-en-US-6/GUID-C2190631-B6F5-4CD7-B6DB-5267DC280E90_3.html + */ + +/* + * Pin mapping + * =========== + * + * QSPI Serial CLK + * + * QSPI CS - Active Low + * + * QSPI IO_0 + * QSPI IO_1 + * QSPI IO_2 + * QSPI IO_3 + */ module qspi_controller ( - // Clock - input wire clk, - - // Reset (active low) - input wire rst_n, - - // Bi-directional I/O - input wire [7:0] uio_in, // IOs: Input path - output wire [7:0] uio_out, // IOs: Output path - output wire [7:0] uio_oe, // IOs: Enable path (active high: 0=input, 1=output) + /* verilog_lint: waive-start port-name-suffix */ + /* Clock. */ + input wire clk, + /* Active-low reset. */ + input wire rst_n, + + /* I/O: input path. */ + input wire [7:0] uio_in, + /* I/O: output path. */ + output wire [7:0] uio_out, + /* I/O: active-high output enable. */ + output wire [7:0] uio_oe + /* verilog_lint: waive-stop port-name-suffix */ ); - // ==================================== - // Pin mapping - // ==================================== - - // QSPI Serial CLK - - // QSPI CS - Active Low - - // QSPI IO_0 - // QSPI IO_1 - // QSPI IO_2 - // QSPI IO_3 - - - logic qspi_clk; - logic qspi_cs_n; - logic [3:0] qspi_data; - - - + logic qspi_clk; + logic qspi_cs_n; + logic [3:0] qspi_data; -endmodule +endmodule : qspi_controller diff --git a/rtl/rv32e_core_wrapper.sv b/rtl/rv32e_core_wrapper.sv index 8d2b5c9..773b7af 100644 --- a/rtl/rv32e_core_wrapper.sv +++ b/rtl/rv32e_core_wrapper.sv @@ -1,8 +1,16 @@ -// Provides a clean, generic bus interface for the core -// Easier UVM access - -module rv32e_core_wrapper (); +/* SPDX-License-Identifier: CERN-OHL-P-2.0 */ +/* + * Copyright 2026 UBC ASIC contributors (Montreal project). + * All rights reserved. + * + * Authors: Chathil Rajamanthree + * + * Montreal RV32E Core Wrapper + * + * Provides a clean, generic bus interface for the core for easier UVM access. + */ +module rv32e_core_wrapper (); -endmodule +endmodule : rv32e_core_wrapper diff --git a/rtl/tt_top.sv b/rtl/tt_top.sv index be5f40d..5f179f6 100644 --- a/rtl/tt_top.sv +++ b/rtl/tt_top.sv @@ -1,58 +1,71 @@ +/* SPDX-License-Identifier: Apache-2.0 OR CERN-OHL-P-2.0 */ + /* - * Copyright (c) 2026 UBC ASIC - * SPDX-License-Identifier: Apache-2.0 + * Copyright 2024 Tiny Tapeout Ltd. + * Copyright 2026 UBC ASIC contributors (Montreal project). + * All rights reserved. + * + * Authors: Tiny Tapeout contributors + * Chathil Rajamanthree + * + * Tiny Tapeout top-level module and QSPI PMOD controller */ -// Core wrapper + QSPI PMOD controller - `default_nettype none -module tt_top ( - // Dedicated inputs - input wire [7:0] ui_in, - - // Dedicated outputs - output wire [7:0] uo_out, - - // Bi-directional I/O - input wire [7:0] uio_in, // IOs: Input path - output wire [7:0] uio_out, // IOs: Output path - output wire [7:0] uio_oe, // IOs: Enable path (active high: 0=input, 1=output) - - // Enable design - input wire ena, // always 1 when the design is powered, so you can ignore it - - // Clock - input wire clk, // clock - - // Reset - input wire rst_n // reset_n - low to reset +/* + * Tiny Tapeout top-level wrapper. + * + * IMPORTANT: The module definition MUST follow the Tiny Tapeout specification + * exactly. Do not modify the port names. + */ +/* verilog_lint: waive module-filename */ +module tt_top_ubc_montreal ( + /* verilog_lint: waive-start port-name-suffix */ + /* Dedicated inputs. */ + input wire [7:0] ui_in, + + /* Dedicated outputs. */ + output wire [7:0] uo_out, + + /* I/O: input path. */ + input wire [7:0] uio_in, + /* I/O: output path. */ + output wire [7:0] uio_out, + /* I/O: active-high output enable. */ + output wire [7:0] uio_oe, + + /* Design enable signal. This will be 1 when the design is powered. */ + input wire ena, + /* Clock. */ + input wire clk, + /* Active-low reset. */ + input wire rst_n + /* verilog_lint: waive-stop port-name-suffix */ ); - // All output pins must be assigned. If not used, assign to 0. - assign uo_out = ui_in + uio_in; // Example: ou_out is the sum of ui_in and uio_in - assign uio_out = 0; - assign uio_oe = 0; - - // List all unused inputs to prevent warnings - wire _unused = &{ena, clk, rst_n, 1'b0}; - + /* Temporary output assignments. Unused pins must be assigned to 0. */ + assign uo_out = ui_in + uio_in; + assign uio_out = '0; + assign uio_oe = '0; - u_rv32e_core_wrapper rv32e_core_wrapper( + /* Connect all unused inputs to prevent warnings. */ + wire unused = &{ena, clk, rst_n, 1'b0}; - ); + rv32e_core_wrapper u_rv32e_core_wrapper (); + qspi_controller u_qspi_controller ( + /* Clock. */ + .clk(), + /* Active-low reset. */ + .rst_n(), - u_qspi_controller qspi_controller( - // Clock - .clk(), - - // Reset - .rst_n(), + /* I/O: input path. */ + .uio_in(), + /* I/O: output path. */ + .uio_out(), + /* I/O: active high output enable. */ + .uio_oe() + ); - // Bi-directional I/O - .uio_in(), // IOs: Input path - .uio_out(), // IOs: Output path - .uio_oe(), // IOs: Enable path (active high: 0=input, 1=output) - ); -endmodule +endmodule : tt_top_ubc_montreal -- cgit v1.2.3