aboutsummaryrefslogtreecommitdiffstats
path: root/testsuite/formal/ram/wbr_ram.sby
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/formal/ram/wbr_ram.sby')
-rw-r--r--testsuite/formal/ram/wbr_ram.sby16
1 files changed, 16 insertions, 0 deletions
diff --git a/testsuite/formal/ram/wbr_ram.sby b/testsuite/formal/ram/wbr_ram.sby
new file mode 100644
index 0000000..84c8081
--- /dev/null
+++ b/testsuite/formal/ram/wbr_ram.sby
@@ -0,0 +1,16 @@
+[tasks]
+bmc
+
+[options]
+bmc: mode bmc
+bmc: depth 10
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 wbr_ram.vhd -e wbr_ram
+prep -top wbr_ram
+
+[files]
+wbr_ram.vhd