| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
* Add formal verification tests with sby to CI
* Fix reviewdog having insufficient API permissions
See-also: #15
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>
|
|
- 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
|
