Hi,
Recently I want to learn something about the SVA/PSL, I found that almost every assertion must specify a clock/default clock to be a trigger for the assertion.
I am confused about that sometimes we probably want to check some asynchronous scenario, like : signal B should be deasserted from 1 to 0 within 60ns after signal A asserted. How could I write a SVA/PSL for this ?
Looking forward to hearing from some real assertion experts.
Thanks,
WangYang
Every assertion needs a leading clocking event to start the evaluation. Also, every variable needs to be sampled by an event. If your timing resolution is 1ns, you’ll need to create a 1ns clock.
import uvm_pkg::*;
`include "uvm_macros.svh"
module m;
timeunit 1ns; timeprecision 100ps;
bit clk; // system clock
bit clk1ns; // the 1 ns clock
initial forever #0.5 clk1ns=!clk1ns;
initial forever #5 clk=!clk;
bit A, B;
// signal B should be deasserted from 1 to 0 within 60ns after signal A asserted.
// Assuming that A is clocked with the clk.
ap_AB: assert property(@(posedge clk) // posedge clk is leading clocking event
$rose(A) |-> @ (posedge clk1ns) ##[1:60] $fell(B) );
initial begin
repeat(2) @(posedge clk);
@(posedge clk) begin
A <= 1'b1;
B <= 1'b1;
end
repeat(30) @(posedge clk1ns);
B<= 1'b0;
repeat(30) @(posedge clk1ns);
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Hi, Ben
Sorry for the late response.
I actually thought about the implementation as you wrote, but what about if the A/B wasn’t not synchronous to the clk ? Which means we probably will miss the event $rose(A) since we only validate the assertion in @posedge clk …
Please feel free to correct me if I was wrong somewhere .
Thanks so much,
WangYang
In reply to caowangyang:
but what about if the A/B wasn’t not synchronous to the clk ?
Then you would need to latch those signals. My initial solution for the reset was to have the assertion reset those latches as shown below. But there are issues here because the latch would set it back if A is not set to 0 prior to the the reset by the assertion. Perhaps an external signal or other logic an do the reset. Anyway, this solution, though problematic, can inspire you at finding something that meets your needs.
import uvm_pkg::*;
`include "uvm_macros.svh"
module masync;
timeunit 1ns; timeprecision 100ps;
bit clk; // system clock
bit clk1ns; // the 1 ns clock
bit A, B, AL, BL;
function void resetAL();
AL=0;
endfunction
function void resetBL() ;
BL=0;
endfunction
initial forever #0.5 clk1ns=!clk1ns;
initial forever #5 clk=!clk;
always_latch begin
if(A) AL=A;
if(B) BL=B;
end
// signal B should be deasserted from 1 to 0 within 60ns after signal A asserted.
// Assuming that A is clocked with the clk.
// THIS SOLUTION HAS ISSUES, see comment above.
ap_AB: assert property(@(posedge clk) // posedge clk is leading clocking event
($rose(AL), resetAL()) |-> @ (posedge clk1ns) ##[1:60] ($fell(BL), resetBL()) );
initial begin
repeat(2) @(posedge clk);
@(posedge clk) begin
A <= 1'b1;
B <= 1'b1;
end
repeat(30) @(posedge clk1ns);
B<= 1'b0;
repeat(30) @(posedge clk1ns);
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Hi Ben,
I have a similar scenario where I want a signal named ‘b’ to be asserted within some time ‘t’ after a signal ‘a’ is asserted. But for my case, the time ‘t’ is variable. I have coded an assertion property like this.
assert property(clk,a,b,t)
@(posedge clk)
$rose(a) |-> ##[1:t] $rose(b);
endproperty
But I am getting the following error:
Error-Illegal use of non-constant expression
The use of a non-constant expression is not allowed in properties, sequences
and assertions for cases such as delay and repetition ranges.
Please replace the offending expression by an elaboration-time constant
Can you please help me out?
Thanks,
Rajesh
In reply to chitturi:
SVA works on events. Your “t” can be a variable of type int using my package with the link below. The “t” is the max number of clocks.
This is SystemVerilog package that facilitates the process of defining in SVA dynamic delays and repeats sequences.
This an item of many requests and confusion at the verification academy forum. Actually, the code is a bit tricky, and the use of a package facilitates the process.
The link below defines the package and a testbench.
https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats
Ben