In reply to caowangyang:
…the @(SAMPCNT) is indeed not a clock event, but seems it could work in my case, because I want this assertion could work whenever SAMPCNT changed
NO, that is not correct.
The @(SAMPCNT) is really fired if SAMPCNT, which is between 0 and 255 (per your requirements), changes from anything other than 0 to 0, or from 0 to anything other than 0. However, going from 5 to 6 is not an event. Also, study my point 2 in my previous response. Doesn’t your counter have a clock? What decrements the counter? a clock?
Without doing detailed analysis of your assertion, this is most likely what you want. You need to check your requirements:
… whenever SAMPCNT changed
$stable returns true if the sampled value of the expression did not change between the sampled value at the previous cycle and the sampled value at the current cycle. Otherwise, it returns false. $changed is a complement to $stable; $changed returns true if the sampled value of the expression changed. Otherwise, it returns false.
[Ben] You should write smaller assertions; they are easier to follow.
//
let a = SAMPCNT; // easier for me to type for now.
// SAMPCNT will be inside 0 ~ 255.
default disable iff !rst_n;
default clocking cb_clk @ (posedge clk); endclocking
a_inside255 : assert property(@(posedge clk) a >=0 && a <255 ); **// <--- UPDATED**
// Once the counter toggled, it will counter down from 255 to 0, previous SAMPCNT always be larger than current SAMPCNT
a_inc : assert property($changed(a) |-> $past(a) > a ); // using the default clocking
// Once the RESETSAMP asserted, the SAMPCNT will be reset to 255.
a_resetcntr : assert property(RESETSAMP |-> a==255);
could you please teach me where I could learn more for the knowledge of “simulation timing region” ?
I previously posted a copy of the section of my SVA book that addresses timing regions at
Timing regions are also in the 1800-21012 LRM
Ben SystemVerilog.us