Below code is not working as per my requirement. Can some one help me out in writing it in a better way and also help me out with the problem in it?
//Functional requirement:
At t1 , a=1, b=x
At t2, b=0
At t3, b=1
At t4, b=0
At t5, b=1
At t6, b=0
At t7, b=x
//Proeprty for the above requirement
property p;
int count = 0;
disable iff(reset == 1'b0)
@(posedge clk)
a |-> ((b === 1'hx), count = 1))
|-> @(posedge b) (`TRUE, count = count - 1'd1)[*0:$]
##1 (count == 0)
|-> @(negedge b) (`TRUE)
|-> @(posedge b) (`TRUE)
|=> (b === 1'bx); //This statement is not getting executed.All others are getting executed
endproperty : p
Can some please tell me why the above line is not getting executed?
Your requirements are not clear. From your first statement about requirements, it is strange to see “X” as a requirement! signals are true or false. If you don’t care about the value, then you can use true for a clock delay. But to require that a signal be an X is unusual; sounds kind of meaningless. Also, when you state t1, t2, etc, you seem to imply a single clock, and all signals (a and b) synchronous to that clock. That is not what you expressed in the assertion.
2)Use to test for an X. $isunknown(expression) returns `true (bit 1’b1) if any bit of the expression is X or Z. This is equivalent to ^(expression) === ’bx.
I can help you with this assertion if ou write in English your requirements.
Ben SystemVerilog.us
The requirement is very clear. I want to check X only. t1, t2 are not clock timings and they are random timings but the assertion should be written with respect to clock and Iam checking for a functionality.
In reply to ben@SystemVerilog.us:
Hi,
The requirement is very clear. I want to check X only. t1, t2 are not clock timings and they are random timings but the assertion should be written with respect to clock and Iam checking for a functionality.
still not clear. Are you saying that signals a, b are clocked with clk?
A requirement would be something like:
Upon a==1, there should be 2 separate rose of b and a fell of b.
Following the fell of b, the signal b goes to unknown state
(that by the way is very strange… can you really guarantee an X?
I really don’t like that $isunknown(a_signal) as a requirement.
Typically, it is used as a if($isunknown(signal)) this_is_an_error.
Can you (out of curiosity) why you check for an X?
a_pab : assert property(@(posedge clk)
a |=> $rose(b)[=2] ##1 $fell(b)[=1] ##1 $isunknown(b)));
// FYI
b[=1] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]
b[=2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]
In reply to ben@SystemVerilog.us:
Ben,
I understands your answer but why (b === 1’bx) is not working? As you mentioned this is not suggested way but is it wrong way.
Thanks
Table 11-9—Definitions of equality operators
a === b a equal to b, including x and z
20.9 Bit vector system functions
$countbits (expression, 'x, 'z) returns the number of bits in expression having values X
or Z.
$isunknown ( expression ) returns true if $countbits(expression,'x,'z)!=0, otherwise it
returns false.
Seems like it should work, unless b is Z
Best bet is to run some simple tests with code without assertions.
Ben