diff options
| author | Tristan Gingold <tgingold@free.fr> | 2020-05-14 18:55:43 +0200 |
|---|---|---|
| committer | Tristan Gingold <tgingold@free.fr> | 2020-05-14 18:55:43 +0200 |
| commit | 35191d291412aace20f6f5fffc22394b8cb6f1b2 (patch) | |
| tree | cc58173a0e49117ce55ed830afa7bd1681b24035 /testsuite/ghdl-issues/issue1309/axis_squarer.sby | |
| parent | 4a3fd93c1a5f72a76fc1a26c2f628224ffe2032b (diff) | |
| download | ghdl-yosys-plugin-35191d291412aace20f6f5fffc22394b8cb6f1b2.tar.gz ghdl-yosys-plugin-35191d291412aace20f6f5fffc22394b8cb6f1b2.tar.bz2 ghdl-yosys-plugin-35191d291412aace20f6f5fffc22394b8cb6f1b2.zip | |
Add test from ghdl/ghdl#1309
Diffstat (limited to 'testsuite/ghdl-issues/issue1309/axis_squarer.sby')
| -rw-r--r-- | testsuite/ghdl-issues/issue1309/axis_squarer.sby | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/testsuite/ghdl-issues/issue1309/axis_squarer.sby b/testsuite/ghdl-issues/issue1309/axis_squarer.sby new file mode 100644 index 0000000..c72c50d --- /dev/null +++ b/testsuite/ghdl-issues/issue1309/axis_squarer.sby @@ -0,0 +1,34 @@ +[tasks] +verify_bmc +prove +cover + +[options] +verify_bmc: mode bmc +verify_bmc: depth 40 +prove: mode prove +prove: depth 20 +cover: mode cover +cover: depth 40 + +[engines] +smtbmc z3 parallel.enable=true + +[script] +ghdl axis_squarer.vhd -e axis_squarer +read_verilog -formal faxis_master.v +read_verilog -formal faxis_slave.v +read_verilog -formal tb_formal_top.v +--pycode-begin-- +cmd = "hierarchy -top tb_formal_top" +if "cover" in tags: + cmd += " -chparam no_backpressure 1" +output(cmd); +--pycode-end-- +prep -top tb_formal_top + +[files] +axis_squarer.vhd +faxis_master.v +faxis_slave.v +tb_formal_top.v |