diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 391fb16..3462c36 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -567,6 +567,7 @@ class SbyTask(SbyConfig): os.makedirs(f"{self.workdir}/model") def print_common_prep(check): + print("scc -select; simplemap; select -clear", file=f) if self.opt_multiclock: print("clk2fflogic", file=f) else: diff --git a/tests/regression/fake_loop.sby b/tests/regression/fake_loop.sby new file mode 100644 index 0000000..419e267 --- /dev/null +++ b/tests/regression/fake_loop.sby @@ -0,0 +1,23 @@ +[options] +mode cover + +[engines] +smtbmc boolector + +[script] +read -formal fake_loop.sv +hierarchy -top fake_loop +proc + +[file fake_loop.sv] +module fake_loop(input clk, input a, input b, output [9:0] x); + wire [9:0] ripple; + reg [9:0] prev_ripple = 9'b0; + + always @(posedge clk) prev_ripple <= ripple; + + assign ripple = {ripple[8:0], a} ^ prev_ripple; // only cyclic at the coarse-grain level + assign x = ripple[9] + b; + + always @(posedge clk) cover(ripple[9]); +endmodule