aboutsummaryrefslogtreecommitdiff
path: root/dv/formal/regfile/regfile.sby
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dv/formal/regfile/regfile.sby (renamed from verif/formal/regfile/regfile.sby)5
1 files changed, 4 insertions, 1 deletions
diff --git a/verif/formal/regfile/regfile.sby b/dv/formal/regfile/regfile.sby
index 69cb7b9..a976a29 100644
--- a/verif/formal/regfile/regfile.sby
+++ b/dv/formal/regfile/regfile.sby
@@ -1,9 +1,12 @@
[tasks]
cover
+bmc
prove
[options]
cover: mode cover
+bmc: mode bmc
+bmc: depth 50
prove: mode prove
prove: depth 20
@@ -20,4 +23,4 @@ prep -top regfile_fv
rtl/types.svh
rtl/config_pkg.sv
rtl/regfile.sv
-verif/formal/regfile/regfile_fv.sv
+dv/formal/regfile/regfile_fv.sv