I am trying to make a simple assertion which checks if two values are equal. Can someone please explain the behaviour when I assign two different values to the same variable
logic src_sig ;
logic dest_sig;
logic alt_sig;
assign a = src_sig;
assign a = alt_sig;
assign b = dest_sig;
My assertion sequence is:
sequence check_seq(X,Y);
(X == Y);
endsequence
And my initial block is:
initial begin
#100 @ (posedge clk) begin
src_sig <= 1;
dest_sig <=1;
alt_sig <= 0;
end
#10 @ (posedge clk) begin
src_sig <=1;
dest_sig <=0;
alt_sig <= 0;
end
#10 @ (posedge clk) begin
src_sig <= 0;
dest_sig <= 0;
alt_sig <= 1;
end
#10 @ (posedge clk) begin
src_sig <= 0;
dest_sig <= 1;
alt_sig <= 1;
end
#30 $finish;
end
I was expecting that the second assignment will override the first one OR it would be assigned to both src_sig
and alt_sig
. So either it should show 2 offences or 4 respectively. But I am getting the following results(3 offences).
"testbench.sv", 31: test.check_assert: started at 103ns failed at 103ns
Offending '(a == b)'
"testbench.sv", 31: test.check_assert: started at 113ns failed at 113ns
Offending '(a == b)'
"testbench.sv", 31: test.check_assert: started at 133ns failed at 133ns
Offending '(a == b)'
Please explain what is happening here?
EDIT:: Complete code
module test_gcc();
logic clk=0;
logic src_sig,dest_sig,alt_sig;
assign a = src_sig;
assign a = alt_sig;
assign b = dest_sig;
initial begin
clk = 0;
forever #1 clk=~clk;
end
sequence check_seq(X,Y);
(X == Y);
endsequence
property check_connection(M,N);
@(posedge clk)
($rose(M)||$rose(N)||$fell(M)||$fell(N)) |-> check_seq(M,N);
endproperty
check_assert : assert property (check_connection(a,b));
initial begin
#100 @ (posedge clk) begin
src_sig <= 1;
dest_sig <=1;
alt_sig <= 0;
end
#10 @ (posedge clk) begin
src_sig <=1;
dest_sig <=0;
alt_sig <= 0;
end
#10 @ (posedge clk) begin
src_sig <= 0;
dest_sig <= 0;
alt_sig <= 1;
end
#10 @ (posedge clk) begin
src_sig <= 0;
dest_sig <= 1;
alt_sig <= 1;
end
#30 $finish;
end
endmodule
a
and b
are 1-bit wire
s, because you have not declared them. (In Verilog/SV, unless you specify default_nettype none
then undeclared objects are wire
s).
If you drive a
wire
from more than one place then a resolution function is executed in order to evaluate the value on thewire
.
In your case, there are two drivers on the wire a
- the two assign
statements. The initial
block ensures that different values are always driven by the two assign
statements, so the resolved value on the wire is always 1'bx
. The value on wire a
never changes.
wire b
is driven by only one assign
statement. The initial
block ensures that it's value changes at 101ns, 111ns and 131ns. The value on wire b
does not change at 121ns.
You have written your property
so that the condition is only checked if there is a change on either wire a
or wire b
:
property check_connection(M,N);
@(posedge clk)
($rose(M)||$rose(N)||$fell(M)||$fell(N)) |-> check_seq(M,N);
endproperty
wire a
never changes and wire b
doesn't change at 121ns, so the condition is not checked at 121ns.