| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
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>
|
|
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>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
The term 'slice' is more consistent with old CPU architectures and
academic literature.
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Closes: #12
Reviewed-by: Warrick Lo <wlo@warricklo.net>
|
|
Implement register file
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
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>
|
|
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Add formal verification files for a simple ALU module.
|
|
- 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
|
|
- 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
|
|
Implements a RISC-V register file with byte-selectable chunk access for
an 8-bit datapath architecture.
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
|
|
Closes: #1
Acked-by: Colin Yeung <colinyeung.main@gmail.com>
Co-authored-by: Chathil Rajamanthree <chathil.rajaman3@gmail.com>
Reviewed-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
Signed-off-by: Warrick Lo <wlo@warricklo.net>
|
|
|
|
|
