I want to do assertion check to make sure req stays high until ack high as shown in the waveform below. I try to do it like this but the assertion fail even when the condition is met. Can someone please point out what’s wrong with my assertion code?
property rfsh_req_wait_for_ack_p;
@(posedge clk)
$rose (dcr_usr_rfsh_req) |-> (dcr_usr_rfsh_req throughout ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
endproperty
rfsh_req_wait_for_ack_a : assert property(rfsh_req_wait_for_ack_p);
In reply to lisa.lalice:
Your assertion does not meet the waveform you display
(dcr_usr_rfsh_req throughout ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
If you want anassertion to meet your waveform where dcr_usr_rfsh_req==0 when
$rose(dsr_usr_rfsh_ack)==1 then do the following:
$rose (dcr_usr_rfsh_req) |->
(dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect
($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
$rose(dsr_usr_rfsh_ack)[->1]
As there is a $rose, isn’t the above assertion successful only in the first clock when ack==1 ?
Should we change the above assertion to as follows:
$rose (dcr_usr_rfsh_req) |->
(dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect
(dsr_usr_rfsh_ack[->1] ##0 $fell(dcr_usr_rfsh_req)));
In reply to yourcheers:
In reply to ben@SystemVerilog.us:
$rose (dcr_usr_rfsh_req) |->
(dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect
(dsr_usr_rfsh_ack[->1] ##0 $fell(dcr_usr_rfsh_req))); // without the $rose
//vs
$rose (dcr_usr_rfsh_req) |->
(dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect
($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req))); // with the $rose
// COMMENTS
a |-> b[->1] // If b==1 in cycle a==1 the property is true
// If b==0 in cycle a==1, then b[->1] is equivalent to $rose(b)[->1]
// because when b==1 you do get a $rose(b).
a |-> $rose(b)[->1] // If b==1 in cycle a==1, then you have to wait till
// b==0 and then rises back to b==1
// Bottom line: Little difference if you know that b==0 when a==1
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
Thanks ben, I was mistaken with the waveform where ack is not a pulse.
In reply to ben@SystemVerilog.us:
If you want anassertion to meet your waveform where dcr_usr_rfsh_req==0 when
$rose(dsr_usr_rfsh_ack)==1 then do the following:
$rose (dcr_usr_rfsh_req) |->
(dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect
($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
Hi Ben, I’ve tried the assertion code you’d suggested me above but my assertion still fail
In reply to lisa.lalice:
Works for me!
ap_reqack: assert property(@(posedge clk)
$rose (req) |->
req[*1:$] ##1 !req intersect
$rose(ack)[->1] ##0 $fell(req));
module top;
timeunit 1ns/10ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, req, ack;
initial forever #10 clk=!clk;
ap_reqack: assert property(@(posedge clk)
$rose (req) |->
req[*1:$] ##1 !req intersect
$rose(ack)[->1] ##0 $fell(req));
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(req, ack) with
{ req dist {1'b1:=5, 1'b0:=1};
ack dist {1'b1:=1, 1'b0:=5};
}) `uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
In reply to ben@SystemVerilog.us:
It seems like my assertion only works when I assert it straight away instead of using property/endproperty
This is what I did and it works
rfsh_req_holds_until_ack_a : assert property(@(posedge clk)
$rose (dcr_usr_rfsh_req) |-> dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect $rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req));
This, on the other hand, the code that I did previously and it fails. It’s actually the same code I’m not sure why it fails
property rfsh_req_wait_for_ack_p;
@(posedge clk)
$rose (dcr_usr_rfsh_req) |->
(dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect
($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
endproperty
rfsh_req_wait_for_ack_a : assert property(rfsh_req_wait_for_ack_p);
In reply to lisa.lalice:
You need either a default clocking or a @(posedge clk) in either the property or in the assertion.
property rfsh_req_wait_for_ack_p;
@(posedge clk $rose (dcr_usr_rfsh_req) |->
(dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect
($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
endproperty
rfsh_req_wait_for_ack_a : assert property(rfsh_req_wait_for_ack_p);
Ben systemverilog.us
In reply to ben@SystemVerilog.us:
Sorry Ben, that is a typo. I did add a default clocking in my assertion code and it still fail.
In reply to lisa.lalice:
Is default clocking the same as @(posedge clk or a different clock.
In reply to ben@SystemVerilog.us:
I used the same clock
In reply to lisa.lalice:
Check your code. If still correct, check with your vendor. The test code below gave me identical results for the whole simulation period. You can try it in your environment.
Also at Edit code - EDA Playground
module top;
timeunit 1ns/10ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, req, ack;
initial forever #10 clk=!clk;
default clocking @(posedge clk);
endclocking
ap_reqack_direct: assert property(@(posedge clk)
$rose (req) |->
req[*1:$] ##1 !req intersect
$rose(ack)[->1] ##0 $fell(req));
property p_reqack_default_clk;
$rose (req) |->
req[*1:$] ##1 !req intersect
$rose(ack)[->1] ##0 $fell(req);
endproperty
ap_reqack_default_clk: assert property(p_reqack_default_clk);
property p_reqack_with_clk;
@(posedge clk) $rose (req) |->
req[*1:$] ##1 !req intersect
$rose(ack)[->1] ##0 $fell(req);
endproperty
ap_reqack_with_clk: assert property(p_reqack_with_clk);
property p_reqack_with_clk2;
$rose (req) |->
req[*1:$] ##1 !req intersect
$rose(ack)[->1] ##0 $fell(req);
endproperty
ap_reqack_with_clk2: assert property(@(posedge clk) p_reqack_with_clk2);
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(req, ack) with
{ req dist {1'b1:=5, 1'b0:=1};
ack dist {1'b1:=1, 1'b0:=5};
}) `uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
// Reesults
...
# ASSERT: Error: ASRT_0005 testbench.sv(10): Assertion "ap_reqack_direct" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(20): Assertion "ap_reqack_default_clk" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(27): Assertion "ap_reqack_with_clk" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(34): Assertion "ap_reqack_with_clk2" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(10): Assertion "ap_reqack_direct" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(20): Assertion "ap_reqack_default_clk" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(27): Assertion "ap_reqack_with_clk" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(34): Assertion "ap_reqack_with_clk2" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)