diff options
| author | Warrick Lo <wlo@warricklo.net> | 2026-06-20 20:39:51 +0000 |
|---|---|---|
| committer | Warrick Lo <wlo@warricklo.net> | 2026-06-20 20:39:51 +0000 |
| commit | d6f2d1744a0e693b14846867a1f1b03d4b853396 (patch) | |
| tree | bf73f64d249190c21f3c35f66149a54e91618b07 /verif/formal/regfile/regfile.sby | |
| parent | Merge branch 'crajaman/top-level-rtl' (diff) | |
| parent | Minor refactor to regfile formal test module (diff) | |
| download | montreal-d6f2d1744a0e693b14846867a1f1b03d4b853396.tar.xz montreal-d6f2d1744a0e693b14846867a1f1b03d4b853396.zip | |
Merge branch 'feature/core'
* feature/core:
Minor refactor to regfile formal test module
Add formal verification for regfile
Move typedefs to types.svh from montreal_pkg
Move design parameters to config_pkg
regfile: refactor: 'chunks' are now 'slices'
See-also: #13
See-also: #14
Reviewed-by: Warrick Lo <wlo@warricklo.net>
Diffstat (limited to 'verif/formal/regfile/regfile.sby')
| -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..69cb7b9 --- /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_fv.sv +prep -top regfile_fv + +[files] +rtl/types.svh +rtl/config_pkg.sv +rtl/regfile.sv +verif/formal/regfile/regfile_fv.sv |