Hi,
I am trying to write an assertion that won’t burden the simulator while checking for x or z on 1000’s of signals. So instead of checking at every posedge of clock I am checking whenever the signal changes.
The following is the code snippet. The expectation is that assertion should fail when there is a transition from 0/1 to x. But the assertion passes.
module output_x_assertion (
input signal1
);
property x_prop_on_d;
@ (signal1)
$changed(signal1) |-> (!$isunknown(signal1));
endproperty
x_prop_on_d_assert : assert property (x_prop_on_d)
`uvm_info("USER_NONX_ASSERT", $psprintf("No X on Signal"), UVM_LOW)
else begin
`uvm_error("USER_NONX_ASSERT","unknown on d")
end
endmodule
Can you let me know where I am going wrong?
Thanks.
In reply to Dilsya:
The issue you have with **assert property (@(a)!$isunknown(a))**is that “a” is sampled in the Preponed Region when “a” changes. Thus, if “a” goes from “1” to “X”, the sampling value is a “1” and thus $isunknown is false. You need the sampling to be in the Active Region.
Use the always with an immediate assertion.
module top;
logic a=1'bX;
event e;
always @(a) begin
$display("%t change in a", $realtime);
a_unknown: assert (!$isunknown(a)) else $display("%t Is unknown in a", $realtime);
-> e;
end
// "a" is sampled in the Preponed Region!
x_prop_on_d_assert : assert property (@(a)!$isunknown(a)) else $display("%t proprIs unknown in a", $realtime);;
initial begin
a=1'bX;
#20 a=1;
#20 a=1'bZ;
#20 a=0;
#20 a=1'bX;
#20 a=0;
#20 a=1;
#20 a=0;
#30;
end
endmodule
20 change in a
# 20 proprIs unknown in a
# 40 change in a
# 40 Is unknown in a
# 60 change in a
# 60 proprIs unknown in a
# 80 change in a
# 80 Is unknown in a
# 100 change in a
# 100 proprIs unknown in a
# 120 change in a
# 140 change in a
Hello Ben, just wondering if the following solution is a valid way of combatting this preponed sampling in a property based assertion (for this application). In this solution the signal is delayed and used for the activation of the property and $isunknown is called on the original signal. Thus, the signal has transitioned and is the desired value when it is sampled.