aboutsummaryrefslogtreecommitdiff
path: root/verif/formal/simple_alu/simple_alu.sby
diff options
context:
space:
mode:
authorWarrick Lo <wlo@warricklo.net>2026-06-17 00:52:01 +0000
committerWarrick Lo <wlo@warricklo.net>2026-06-17 00:52:01 +0000
commit81ca21e0db518bb45d6a60beb3bfc927bb95da62 (patch)
tree719251f1bbdfe4c6aa436a89d58aacbaceeb6596 /verif/formal/simple_alu/simple_alu.sby
parentMove design parameters to config_pkg (diff)
parentMerge branch 'crajaman/top-level-rtl' (diff)
downloadmontreal-81ca21e0db518bb45d6a60beb3bfc927bb95da62.tar.xz
montreal-81ca21e0db518bb45d6a60beb3bfc927bb95da62.zip
Sync with 'master'
Signed-off-by: Warrick Lo <wlo@warricklo.net>
Diffstat (limited to '')
-rw-r--r--verif/formal/simple_alu/simple_alu.sby22
1 files changed, 22 insertions, 0 deletions
diff --git a/verif/formal/simple_alu/simple_alu.sby b/verif/formal/simple_alu/simple_alu.sby
new file mode 100644
index 0000000..cd028d9
--- /dev/null
+++ b/verif/formal/simple_alu/simple_alu.sby
@@ -0,0 +1,22 @@
+[tasks]
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+depth 100
+
+[engines]
+smtbmc
+
+[script]
+read -formal -sv simple_alu.sv
+read -formal -sv simple_alu_fv.sv
+read -formal -sv simple_alu_top_fv.sv
+prep -top simple_alu_top_fv
+
+[files]
+../../../rtl/simple_alu.sv
+simple_alu_fv.sv
+simple_alu_top_fv.sv