System verilog Assertion

SystemVerilog
1

Q. For below code I an getting error at @25 without check complete sequnce how tool can through error?

`timescale 1ns/1ps

module axi_awaddr_assertion_tb;

// Signals
logic clk;
logic rst_n;
logic awvalid;
logic awready;
logic \[31:0\] awaddr;

// Clock generation
initial clk = 0;
always #5 clk = \~clk; // 100 MHz clock

// Reset and stimulus
initial begin
rst_n = 0;
awvalid = 0;
awready = 0;
awaddr = 32’h0;
#20;
rst_n = 1;
end

initial begin
@(posedge rst_n);

// VALID AXI behavior (PASS)
// ---
@(posedge clk);
awvalid = 1;
awaddr = 32'hDEADBEEF;

// Hold address stable while AWREADY = 0
repeat (3) @(posedge clk);

awready = 1; // Handshake
@(posedge clk);

awvalid = 0;
awready = 0;

// ---
// INVALID AXI behavior (to see FAIL)
// ---

@(posedge clk);
awvalid = 1;
awaddr = 32'hAAAA5555;

@(posedge clk);
awaddr = 32'hBBBB6666; // ILLEGAL CHANGE - should fail assertion

@(posedge clk);
awready = 1;

#50;
$finish;

end

// —
// AXI ASSERTION
// —
property awaddr_stable_when_valid;
@(posedge clk)
disable iff (!rst_n)
(awvalid && !awready) ##1(awaddr);
endproperty

// Assertion instance
assert property (awaddr_stable_when_valid)
else $error(“AXI AWADDR changed while AWVALID=1 and AWREADY=0”);

// Waveform dumping
initial begin
$dumpfile(“wave.vcd”);
$dumpvars();
end

endmodule

/*
axi_awaddr_assertion_tb
Loading snapshot worklib.axi_awaddr_assertion_tb:sv … Done
xcelium> source /xcelium23.09/tools/xcelium/files/xmsimrc
xcelium> run
xmsim: *E,ASRTST (./testbench.sv,73): (time 25 NS) Assertion axi_awaddr_assertion_tb.awaddr_stable_when_valid has failed
AXI AWADDR changed while AWVALID=1 and AWREADY=0
xmsim: *E,ASRTST (./testbench.sv,73): (time 65 NS) Assertion axi_awaddr_assertion_tb.awaddr_stable_when_valid has failed
AXI AWADDR changed while AWVALID=1 and AWREADY=0
xmsim: *E,ASRTST (./testbench.sv,73): (time 75 NS) Assertion axi_awaddr_assertion_tb.awaddr_stable_when_valid has failed
AXI AWADDR changed while AWVALID=1 and AWREADY=0
xmsim: *E,ASRTST (./testbench.sv,73): (time 105 NS) Assertion axi_awaddr_assertion_tb.awaddr_stable_when_valid has failed
AXI AWADDR changed while AWVALID=1 and AWREADY=0
xmsim: *E,ASRTST (./testbench.sv,73): (time 115 NS) Assertion axi_awaddr_assertion_tb.awaddr_stable_when_valid has failed
AXI AWADDR changed while AWVALID=1 and AWREADY=0
xmsim: *E,ASRTST (./testbench.sv,73): (time 125 NS) Assertion axi_awaddr_assertion_tb.awaddr_stable_when_valid has failed
AXI AWADDR changed while AWVALID=1 and AWREADY=0
xmsim: *E,ASRTST (./testbench.sv,73): (time 135 NS) Assertion axi_awaddr_assertion_tb.awaddr_stable_when_valid has failed
AXI AWADDR changed while AWVALID=1 and AWREADY=0
Simulation complete via $finish(1) at time 145 NS + 0
./testbench.sv:59 $finish;
xcelium> exit
TOOL: xrun 23.09-s001: Exiting on Dec 27, 2025 at 04:47:31 EST (total: 00:00:01)
Exit code expected: 0, received: 1

*/

image
image1045×198 27.2 KB

2

This is because concurrent assertions use sampled values of the variables

In active region of T:25ns you assign awvalid as 1. It’s preponed value is 0.

Also note that you haven’t use implication operator ( |→ / |=> ) in your property

Your code would require awvalid to be asserted and awready to be de-asserted on each clocking event, else your assertion would fail ( like it does at T:25 ns )

Given the intention you should write the property as

property awaddr_stable_when_valid;
 @(posedge clk) disable iff (!rst_n)
  $rose(awvalid) && !awready |=> $stable(awaddr) throughout awready[->1];
endproperty

The stability check makes sense only when awready is low when awvalid is asserted.

If awready is asserted before / at the same time as awvalid, the handshake would occur on the very 1st clocking event ( called as single cycle transfer )

3

Thank you for the reply. I already know the correct solution. Actually, by mistake I encountered this scenario, and then I started trying to understand why this failure was occurring.

“Your code would require awvalid to be asserted and awready to be de-asserted on each clocking event; otherwise, your assertion would fail (as it does at T = 25 ns).”—> at what region of T=25ns

So, the evaluation of the concurrent assertion on observed region is based on the sampled values in the preponed region. Even if the signals change later in the active region, that does not affect the assertion result. Is this what you meant?

I am confused how correct execution will occur, in which region it will gothrough.

4

That statement is for the most part correct. If the signals change in any region after the preponed region, it wouldn’t affect the assertion evaluation because the signal’s value was sampled in the preponed region.

You’d gain a clearer understanding of the situation if you applied the stimulus at the negative edge of the clock.

5

I am not clear whether you meant to ask “which region the assertion would fail“ or “which region is used for sampling“

Pass / Fail action block executes in reactive region whereas the sampled values are from preponed region ( before any assignments are made in active region )