mirror of https://github.com/YosysHQ/yosys.git
Merge pull request #4724 from YosysHQ/micko/blackbox_verific
verific: fix blackbox regression and add test case
This commit is contained in:
commit
29e8812bab
|
@ -3422,6 +3422,7 @@ struct VerificPass : public Pass {
|
||||||
RuntimeFlags::SetVar("veri_preserve_assignments", 1);
|
RuntimeFlags::SetVar("veri_preserve_assignments", 1);
|
||||||
RuntimeFlags::SetVar("veri_preserve_comments", 1);
|
RuntimeFlags::SetVar("veri_preserve_comments", 1);
|
||||||
RuntimeFlags::SetVar("veri_preserve_drivers", 1);
|
RuntimeFlags::SetVar("veri_preserve_drivers", 1);
|
||||||
|
RuntimeFlags::SetVar("veri_create_empty_box", 1);
|
||||||
|
|
||||||
// Workaround for VIPER #13851
|
// Workaround for VIPER #13851
|
||||||
RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
|
RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
|
||||||
|
|
|
@ -0,0 +1,24 @@
|
||||||
|
verific -sv -lib <<EOF
|
||||||
|
module TEST_CELL(input clk, input a, input b, output reg c);
|
||||||
|
parameter PATH = "DEFAULT";
|
||||||
|
always @(posedge clk) begin
|
||||||
|
if (PATH=="DEFAULT")
|
||||||
|
c <= a;
|
||||||
|
else
|
||||||
|
c <= b;
|
||||||
|
end
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
EOF
|
||||||
|
|
||||||
|
verific -sv <<EOF
|
||||||
|
module top(input clk, input a, input b, output c, output d);
|
||||||
|
TEST_CELL #(.PATH("TEST")) test1(.clk(clk),.a(a),.b(1'b1),.c(c));
|
||||||
|
TEST_CELL #(.PATH("DEFAULT")) test2(.clk(clk),.a(a),.b(1'bx),.c(d));
|
||||||
|
endmodule
|
||||||
|
EOF
|
||||||
|
|
||||||
|
verific -import top
|
||||||
|
hierarchy -top top
|
||||||
|
stat
|
||||||
|
select -assert-count 2 t:TEST_CELL
|
Loading…
Reference in New Issue