aboutsummaryrefslogtreecommitdiff
path: root/rtl/tt_top.sv (unfollow)
AgeCommit message (Collapse)AuthorFilesLines
2026-06-20Minor refactor to regfile formal test modulefeature/coreWarrick Lo2-56/+83
Signed-off-by: Warrick Lo <wlo@warricklo.net>
2026-06-18Add formal verification for regfileWarrick Lo2-0/+244
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 <wlo@warricklo.net>
2026-06-18Move typedefs to types.svh from montreal_pkgWarrick Lo4-13/+27
Yosys has poor support of packaged types. We will move typedefs to header files to prepare for formal verification with sby and the Tiny Tapeout flow later on, which uses yosys. Additionally, a debug port has been exposed to help verify the internal state of the regfile registers. Signed-off-by: Warrick Lo <wlo@warricklo.net>
2026-06-17Move design parameters to config_pkgWarrick Lo3-10/+37
Signed-off-by: Warrick Lo <wlo@warricklo.net>
2026-06-16regfile: refactor: 'chunks' are now 'slices'Warrick Lo1-14/+14
The term 'slice' is more consistent with old CPU architectures and academic literature. Signed-off-by: Warrick Lo <wlo@warricklo.net>
2026-06-15Add asynchronous reset to register fileWarrick Lo1-1/+4
Signed-off-by: Warrick Lo <wlo@warricklo.net>
2026-06-14Rename top-level module to prevent clashesWarrick Lo3-85/+115
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 <wlo@warricklo.net>
2026-06-14Add top-level and QSPI controller modulesChat3-0/+104
2026-05-27Update README and WaveDrom diagrams [skip ci]Warrick Lo49-93/+295
Signed-off-by: Warrick Lo <wlo@warricklo.net>
2026-05-23Add WaveDrom diagrams for instructions to READMEWarrick Lo1-22/+28
Signed-off-by: Warrick Lo <wlo@warricklo.net>
2026-05-19Pass linterChat4-62/+83
- 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
2026-05-14Add simple_alu RTL and formal verificationChat9-0/+189
- 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