diff --git a/tests/regression/verilog_hier_path.sby b/tests/regression/verilog_hier_path.sby new file mode 100644 index 00000000..fcb45c74 --- /dev/null +++ b/tests/regression/verilog_hier_path.sby @@ -0,0 +1,27 @@ +[options] +mode bmc +depth 1 +expect fail + +[engines] +smtbmc + +[script] +read_verilog -formal sub.v +read_verilog -formal top.v +prep -top \\(foo) + +[file top.v] +module \\(foo) (input a); + always @* begin + assert_foo: assert (a); + end + \\(bar) \\(bar)=i= (.a(a)); +endmodule + +[file sub.v] +module \\(bar) (input a); + always @* begin + assert_bar: assert (a); + end +endmodule diff --git a/tests/regression/vhdl_hier_path.sby b/tests/regression/vhdl_hier_path.sby index cbc78908..7b8c64ca 100644 --- a/tests/regression/vhdl_hier_path.sby +++ b/tests/regression/vhdl_hier_path.sby @@ -12,6 +12,7 @@ verific -vhdl sub.vhd verific -vhdl top.vhd hierarchy -top top hierarchy -top \\sub(p=41)\(rtl) +prep [file top.vhd] library ieee;