I am an SVA beginner and I haven’t been able to figure out this odd (to me!) behavior. Any insights appreciated!
Whenever state changes, I simply want to check that b is 0 at that instant (preponed value fine). This probably seems weird, but I don’t have access to the clock in this case.
With the option 1 line uncommented below, the assertion works as I expect and runs successfully at every state change where state isn’t 00 (at times 1us, 2us and 3us). But, when I uncomment option 2 line instead (which I thought would have the same functionality) the assertion finishes only once (at 1us) and doesn’t check at 2us and 3us. Any idea why?
module top;
logic [2:0] state=3'b001;
logic b = 0;
initial
begin
#1us;
state = 3'b010;
#1us
state = 3'b011;
#1us;
state = 3'b100;
#1us;
$finish;
end
property myprop;
@(state[2], state[1], state[0])
(state!=3'b00, $display("checking")) |-> (b==1'b0); // option 1 - checks all state changes
//(state!=3'b00) |-> (b==1'b0); // option 2 - only checks first state change?
endproperty
assert property (myprop) $display("passed at %t",$realtime);
else $display("failed at %t",$realtime);
endmodule
**Running with option 1:
**
xcelium> run
checking
passed at 1000
checking
passed at 2000
checking
passed at 3000
Simulation complete via $finish(1) at time 4 US + 0
./testbench.sv:15 $finish;
**Running with option 2:
**
xcelium> run
passed at 1000
Simulation complete via $finish(1) at time 4 US + 0
./testbench.sv:15 $finish;
xcelium> exit
TOOL: xrun 20.09-s003: Exiting on Jun 09, 2022 at 11:07:19 EDT (total: 00:00:02)
In reply to John Canfield:
If you have a clock that changes the values of the states, then the clocking event should be that clock. If you are talking about an asynchronous state machine, then your
@(state!=3’b00) means that the clocking event for the assertion is whenever
states changes from 0 to a value unequal to 0 (i.e., 1, 2,…7), or vice versa.
In other words, the @(state!=3’b00) has an event when the expression (state!=3’b00)
transitions to 1 or transitions to 0. If that expression stalls at 0 ot 1, then thre is no clocking event.
I thought the @(state[2], state[1], state[0]) would establish the clocking (essentially a clock event any time any one of those signals changed state)? I guess that is not the case?
Also, any idea why the property does seem to finish on any state change when the seemingly superfluous $display statement is added to it? Shouldn’t your argument still hold true - that it should only get a clocking even on a transition out of state in or out of state==0?
Also, why does the assertion execute/finish at t=1us, when the state is changing from 1 to 2 at which time the expression (state!=3’b000) should be constantly equal to 1?
I thought the @(state[2], state[1], state[0]) would establish the clocking (essentially a clock event any time any one of those signals changed state)? I guess that is not the case?
It is the case, per 1800’2017 9.4.2.1 Event OR operator
Also, any idea why the property does seem to finish on any state change when the seemingly superfluous $display statement is added to it?
Shouldn’t your argument still hold true - that it should only get a clocking even on a transition out of state in or out of state==0?
It does. Note: #1us state=3’b001; #1us state = 3’b010;
At the 2us, when state transitions to 3’b010 the sampling value of state is 3’b001.
Thank you for the help, but I still don’t think I understand. In the following example, why does mypropGOOD work (finishes at 1us, 2us, 3us, 4us) but mypropBAD does not (finishes ONLY at 1us)?:
module top;
logic [2:0] state = 3'b001;
logic b = 0;
initial
begin
#1us state = 3'b010;
#1us state = 3'b011;
#1us state = 3'b100;
#1us state = 3'b101;
#1us $finish;
end
// doesn't work (I think)
property mypropBAD;
@(state[2], state[1], state[0]) (state!=3'b000) |-> (b==1'b0);
endproperty
pbad: assert property (mypropBAD) $display("mypropBAD passed at %t",$realtime);
else $display("mypropBAD failed at %t",$realtime);
// works
property mypropGOOD;
@(state[2], state[1], state[0]) (state!=3'b000) |-> (b==1'b0, $system("") );
endproperty
pgood: assert property (mypropGOOD) $display("mypropGOOD passed at %t",$realtime);
else $display("mypropGOOD failed at %t",$realtime);
endmodule
Simulator Output for above:
mypropGOOD passed at 1000
mypropBAD passed at 1000
mypropGOOD passed at 2000 [why didn't mypropBAD finish here too?]
mypropGOOD passed at 3000 [why didn't mypropBAD finish here too?]
mypropGOOD passed at 4000 [why didn't mypropBAD finish here too?]
Why do mypropBAD and mypropGOOD work differently when the only difference is a $system(“”) call which does nothing?
It looks like that is the correct answer, thanks. It is tool dependent:
# mypropBAD passed at 1000
# mypropGOOD passed at 1000
# mypropGOOD passed at 2000
# mypropGOOD passed at 3000
# mypropGOOD passed at 4000
# Info: RUNTIME_0068 testbench.sv (11): $finish called.
# Time: 5 us, Iteration: 0, Instance: /top, Process: @INITIAL#5_0@.
# stopped at time: 5 us
mypropGOOD passed at 1000
mypropBAD passed at 1000
mypropGOOD passed at 2000
mypropGOOD passed at 3000
mypropGOOD passed at 4000
Simulation complete via $finish(1) at time 5 US + 0
# mypropGOOD passed at 1000
# mypropBAD passed at 1000
# mypropGOOD passed at 2000
# mypropBAD passed at 2000
# mypropGOOD passed at 3000
# mypropBAD passed at 3000
# mypropGOOD passed at 4000
# mypropBAD passed at 4000
# ** Note: $finish : testbench.sv(11)
# Time: 5 us Iteration: 0 Instance: /top
mypropBAD passed at 0
mypropGOOD passed at 0
mypropBAD passed at 1000
mypropGOOD passed at 1000
mypropBAD passed at 2000
mypropGOOD passed at 2000
mypropBAD passed at 3000
mypropGOOD passed at 3000
mypropBAD passed at 4000
mypropGOOD passed at 4000
$finish called from file "testbench.sv", line 11.
$finish at simulation time 5000
Thanks for the info.
Please note that we DO NOT DISCUSS TOOLS in this forum.
If there is a tool issue, avoid naming the tool; you can talk about
the malfunction in a more generic manner, like “it worked
with tool A, but failed with tool B”.
The purpose of this forum is to address language usages, understandings,
approaches to technical requirements, solutions, etc…
EDA playground is neat, but IMHO, if we start talking about
vendors’ issues we may lose the access.
Okay, understood and sorry about that. I just thought it might be helpful info for others who run into the issue, but I understand and have edited my posts as you suggest. Thanks.