montreal/verif/formal, branch feature/fu

Add CI pipeline for formal verification

2026-06-24T07:58:06+00:00

* Add formal verification tests with sby to CI * Fix reviewdog having insufficient API permissions See-also: #15 Signed-off-by: Warrick Lo

Minor refactor to regfile formal test module

2026-06-20T11:50:19+00:00

Signed-off-by: Warrick Lo

Add formal verification for regfile

2026-06-19T06:20:11+00:00

Successfully verifies the following requirements: * REQ-REGFILE-010 * 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-053 * REQ-REGFILE-060 Verified through construction of regfile: * REQ-REGFILE-040 See-also: #14 Signed-off-by: Warrick Lo

Pass linter

2026-05-19T08:31:06+00:00

- 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

Add simple_alu RTL and formal verification

2026-05-15T02:58:51+00:00

- 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