mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 11:42:30 +00:00
Code Activity

Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF

Browse source
This commit is contained in:
Clifford Wolf 2018-02-15 15:26:37 +01:00
parent c1abd3b02c
commit bc8ab3ab44
2 changed files with 35 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
frontends/verific/verific.cc
View file

@ -1350,7 +1350,7 @@ struct VerificSvaPP
return default_net;
}
if (inst->Type() == PRIM_SVA_AT) {
if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
Net *new_net = rewrite(get_ast_input2(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput2());

34
tests/sva/sva_not.sv Normal file
View file

@ -0,0 +1,34 @@
module top (
input clk,
input reset,
input ping,
input [1:0] cfg,
output reg pong
);
reg [2:0] cnt;
localparam integer maxdelay = 8;
always @(posedge clk) begin
if (reset) begin
cnt <= 0;
pong <= 0;
end else begin
cnt <= cnt - |cnt;
pong <= cnt == 1;
if (ping) cnt <= 4 + cfg;
end
end
assert property (
@(posedge clk)
disable iff (reset)
not (ping ##1 !pong [*maxdelay])
);
`ifndef FAIL
assume property (
@(posedge clk)
not (cnt && ping)
);
`endif
endmodule