In reply to caowangyang:
My mistake on how the @count vector works; you’re correct in that, but I rarely use the @ of a vector. However, you need to understand the difference between sampled and current value. Consider the following example
module atcount;
bit clk, a;
bit[2:0] count;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
always_ff @ (posedge clk)
count <= count+1'b1;
always @ (count) begin
$display("current count=%b, sampled count=%b", count, $sampled(count));
end
endmodule : atcount
Simulation produced the following results:
run 100ns
# current count=001, sampled count=000
# current count=010, sampled count=001
# current count=011, sampled count=010
# current count=100, sampled count=011
# current count=101, sampled count=100
When you do
assert property ( @(SAMPCNT) (!$isunknown(SAMPCNT)) |->
( SAMPCNT >= 0 && SAMPCNT <= 255 )
// The !$isunknown(SAMPCNT), SAMPCNT >= 0 , etc is NOT the current value of SAMPCNT, but the sammpled value of SAMPCNT. Thus, you need to understand the following
a_ : assert property(@(a) a);
// If posedge(a) , then (a) is sampled just before the posedge, i.e., (a)==0
// If negedge(a), then (a) is sampled just before the negedge, i.e., (a)==1
The @(a) means that the clocking event for the assertion is at both edges
In any case, it is not correct to use the @(signal) as the clocking event.
If you want to create your own reality, vision, or doctorate paper on this issue, please be my guest. However, this is NOT how SVA is used. In fact, most users prefer small assertions, and the clocking event is the clock edge that produces the change.
BTW, I updated
a_inside255 : assert property(@(posedge clk) a >=0 && a <255 ); **// <--- UPDATED**
Ben SystemVerilog.us