diff options
| author | Warrick Lo <wlo@warricklo.net> | 2026-06-18 23:20:11 -0700 |
|---|---|---|
| committer | Warrick Lo <wlo@warricklo.net> | 2026-06-18 23:20:11 -0700 |
| commit | c8261a040bf328d4d2296f0c91a85a4193195844 (patch) | |
| tree | 0d4a1d10280fbd7ceee8ab78fdaf3067a8eb6bae /verif/formal/regfile/regfile.sby | |
| parent | Move typedefs to types.svh from montreal_pkg (diff) | |
| download | montreal-c8261a040bf328d4d2296f0c91a85a4193195844.tar.xz montreal-c8261a040bf328d4d2296f0c91a85a4193195844.zip | |
Add formal verification for regfile
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>
Diffstat (limited to '')
| -rw-r--r-- | verif/formal/regfile/regfile.sby | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby new file mode 100644 index 0000000..89f8884 --- /dev/null +++ b/verif/formal/regfile/regfile.sby @@ -0,0 +1,23 @@ +[tasks] +cover +prove + +[options] +cover: mode cover +prove: mode prove +prove: depth 20 + +[engines] +smtbmc + +[script] +read -formal -sv config_pkg.sv +read -formal -sv regfile.sv +read -formal -sv regfile_ind.sv +prep -top regfile_ind + +[files] +rtl/types.svh +rtl/config_pkg.sv +rtl/regfile.sv +verif/formal/regfile/regfile_ind.sv |