I was trying to create assertion coding to catch the invalid condition as shown in picture.
it seems like no straight forward assertion could do this check.
differentiate clock need at least an ack pulse throughout the error section.
other parts of the waveform are acceptable.
In reply to ChChee:
Your requirements are ambiguous, but reading through the lines, you seem to be saying that upon a request you did not receive an ack though there were clocks.
differentiate clock need at least an ack pulse throughout the error section.
What does that mean?
What was your assertion? I see it as:
ap_req_ack: assert property(@ (posedge clk) $rose(req) |->
##[1:8] ack ); // guessing at that 8
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:
Yes Ben, we should get an ack after req and also clk-signal toggles.
requirement are:
this is a back to back req, that’s why we saw previous clk running in current req.
this clk is a signal , it’s not the sampling clock (few GHz).
I was thinking to write this, but obviously it’s not going to work:
assert_b2b_check_missing_ack: assert property (@(posedge sampling_clock) b2b_check_missing_ack));
property b2b_check_missing_ack;
//code here are conceptual only, it's not a working codes
@(posedge clk) $past(clk) == 0 |-> (##[0:$] changed(clk)) && req && !ack |-> !( (##[0:$] $stable(clk)) && req && !ack )
endproperty
the focus of the codes was to catch missing ack throughout clk start to stop running.
the difficulty here is that we have continuous stream of clk, req and ack. checking has to take care of the overlapping of all these signals.
In reply to ChChee:
I wanted to screen the condition below (missing ack=1) in a sequence of:
In reply to ChChee:
You can write an assertion using the sampling_clock as your main clocking event and use req, ack, and clk as the module variables. The relationship between the clocking event and clk is not clear. Below are 2 solutions. The fork-join_any solution allows you to tune the assertion to your requirements.
module top;
timeunit 1ns; timeprecision 100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit sampling_clock, clk, req, ack;
event e0, e1, e2, e3, e4;
//assert_b2b_check_missing_ack: assert property (@(posedge sampling_clock) b2b_check_missing_ack);
//property b2b_check_missing_ack; // *** the clocking event is @(posedge clk) and not the sampling_clock
//code here are conceptual only, it's not a working codes
// @(posedge clk) $past(clk) == 0 |-> (##[0:$] changed(clk)) && req && !ack |-> !( (##[0:$] $stable(clk)) && req && !ack )
//endproperty
/* I wanted to screen the condition below (missing ack=1) in a sequence of:
1. clk off && req=1 && ack=0
2. clk active && req=1 && ack=0
3. clk off && req=1 && ack=0 */
/* - after req asserted, followed by at least 3 clk prior to ack assertion
- after req de-asserted, ack should also de-assert and followed by at least 3 clk pulses before clk off
- residue clk from previous req running in current req is allowed */
let tmax=10; // number of clk cycles after ($rose(req) && !ack)
// Possible assertion
ap: assert property(@ (posedge sampling_clock)
$rose(req) && !ack |-> ##[1:tmax] ack);
// Solution that can be more finely tuned.
task automatic checkack();
bit tmax_end, ack_end;
fork
fork1: begin
-> e0; // for debug
repeat(tmax) @(posedge clk);
tmax_end = 1'b1;
-> e1;
disable fork2;
end
fork2: begin
@(ack);
ack_end=1'b1;
-> e2;
disable fork1;
end
join_any
// $display("%t @join %t, err=%b", $realtime, $realtime, err);
if(tmax_end && !ack_end) begin
a_ackerr: assert (0);
-> e3;
end
endtask
always @(posedge sampling_clock) if($rose(req) && !ack) checkack();
endmodule
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
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
In reply to ben@SystemVerilog.us:
the fork join idea is good.
bit clock_status;
always @(sampling_clock)
fork
begin
@(posedge clock)
#1ps;
if(clock !== 1'bx && clock !==1'bz) clock_status = 1;
end
begin
#(period *1.01);
clock_status = 0;
end
join_any
disable_fork;
end
i converted the clock streams to single pulse and things got easier for detection.
but one weird thing happened, there are additional clock_status pulses. This event occurred after some time (consistent time) clock changed from x to 0.
