aboutsummaryrefslogtreecommitdiff
path: root/verif/formal/regfile/regfile.sby
diff options
context:
space:
mode:
authorWarrick Lo <wlo@warricklo.net>2026-07-07 06:01:17 +0000
committerWarrick Lo <wlo@warricklo.net>2026-07-07 06:01:17 +0000
commit6c24f49f3239c79173fd180d065f8f03cfaeabfd (patch)
tree4ac1ebc964784b655cda35de979331196b19a3c2 /verif/formal/regfile/regfile.sby
parentMerge branch 'feature/fu' from MyDariell (diff)
parentAdd DCO [skip ci] (diff)
downloadmontreal-6c24f49f3239c79173fd180d065f8f03cfaeabfd.tar.xz
montreal-6c24f49f3239c79173fd180d065f8f03cfaeabfd.zip
Sync with 'master'feature/fu
Signed-off-by: Warrick Lo <wlo@warricklo.net>
Diffstat (limited to 'verif/formal/regfile/regfile.sby')
-rw-r--r--verif/formal/regfile/regfile.sby23
1 files changed, 0 insertions, 23 deletions
diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby
deleted file mode 100644
index 69cb7b9..0000000
--- a/verif/formal/regfile/regfile.sby
+++ /dev/null
@@ -1,23 +0,0 @@
-[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