diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4ea7a442..ebb11f5a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -44,6 +44,7 @@ jobs: echo "ENABLE_VERIFIC := 1" >> Makefile.conf echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1" >> Makefile.conf echo "ENABLE_CCACHE := 1" >> Makefile.conf make -j${{ env.procs }} make install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX= diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index 185ed449..ffb827c1 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -146,12 +146,12 @@ def find_property(self, path, cell_name, trans_dict=dict()): path_iter = iter(path) mod = next(path_iter).translate(trans) - if self.name != mod: + if self.name.translate(trans) != mod: raise ValueError(f"{self.name} is not the first module in hierarchical path {pretty_path(path)}.") mod_hier = self for mod in path_iter: - mod_hier = next((v for k, v in mod_hier.submodules.items() if mod == k.translate(trans)), None) + mod_hier = next((v for k, v in mod_hier.submodules.items() if mod.translate(trans) == k.translate(trans)), None) if not mod_hier: raise KeyError(f"Could not find {pretty_path(path)} in design hierarchy!") 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 new file mode 100644 index 00000000..7b8c64ca --- /dev/null +++ b/tests/regression/vhdl_hier_path.sby @@ -0,0 +1,97 @@ +[options] +mode bmc +depth 1 +expect fail + +[engines] +smtbmc + +[script] +verific -vhdl subsub.vhd +verific -vhdl sub.vhd +verific -vhdl top.vhd +hierarchy -top top +hierarchy -top \\sub(p=41)\(rtl) +prep + +[file top.vhd] +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity top is + port ( + a : in integer + ); +end entity; + +architecture rtl of top is +component sub is + generic ( + p : integer + ); + port ( + a : in integer + ); +end component; +begin + sub_i: sub + generic map ( + p => 41 + ) + port map ( + a => a + ); +end architecture; + +[file sub.vhd] +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity sub is + generic ( + p : integer := 99 + ); + port ( + a : in integer + ); +end entity; + +architecture rtl of sub is +component subsub is + generic ( + p : integer + ); + port ( + a : in integer + ); +end component; +begin + subsub_i: subsub + generic map ( + p => p + 1 + ) + port map ( + a => a + ); +end architecture; + +[file subsub.vhd] +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity subsub is + generic ( + p : integer := 99 + ); + port ( + a : in integer + ); +end entity; + +architecture rtl of subsub is +begin + assert (p > a); +end architecture;