In reply to ben@SystemVerilog.us:
Is it possible to use a variable along with $past construct ?
property sig_high_check;
int high_value;
@(posedge clk)
($rose(signal_b), high_value = signal_a_reg) |-> $past($rose(signal_a),high_value);
endproperty
Throws error - variable can’t use along with $past.
The issue is not the $past, but your syntax in the use of the $past.
The syntax of the function is: [1]
$past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
More explanation from my SVA Handbook 4th Edition
Here is what I believe you wanted to express:
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b, e;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
property p;
bit d;
($rose(a), d=b) |-> $past($rose(b)) ##0 d==e;
endproperty
ap: assert property(p);
initial begin
repeat(20) begin
@(posedge clk);
if (!randomize(a, b, e) with
{ a dist {1'b1:=1, 1'b0:=3};
b dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
endmodule
What is the varible e ? why it’s used in your code
Few clarifications
sig_a ( 1 bit) is input, sig_b ( 1 bit) is output when ever there is change in sig_b,(rise or fall) sig_a should have risen or fell, before the programmed number of cycles. Mentioned only positive case above.
Valiable delay ( programmed numbebr of cycles) is bit [7:0] for both rise duration and fall duration for sig_a
Confused on the implementation as per the syntax mentioned in
($rose(a), d= delay) |=> $past (a==b, d,1,@(rose(b))); // Is the correct usage
or
($rose (b), d= delay ) |=> $past(a==b, d, 1 , @(rose(b)));
Expression 1 checks a==b, before d cycles, 1 is enable condition, @ clocking event , which is rise of signal b.
I misinterpreted your requirements.
Getting back to your code:
($rose(a), d= delay) |=> $past (a==b, d,1,@(rose(b))); // Is the correct usage
That is the ICORRECT usage of $past because the # of ticks must be static, Youe have it as “d”, which is a variable and is dynamic, known at runtime, not elaboration time.
Per spec, and explained in my book http://systemverilog.us/vf/svabk4_past.pdf
The syntax of the function is: [1] $past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
expression1 represents the expression being sought.
The three optional arguments define the following:
expression1 and expression2 can be any expression allowed in assertions. number_of_ticks specifies the number of clock ticks in the past. number_of_ticks must be one or greater, and must be static (i.e., known at elaboration time). If number_of_ticks is not specified, then it defaults to 1. If the specified clock tick in the past is before the start of simulation, the returned value from the $past function is a value of X
As a guideline, it is best to write assertions that go forward, meaning
antecedent |-> present_or_future_expectations
instead of
antecedent |-> some_past_occurences
Hopefully, you also read my paper that explains the engine behind SVA. You should be able to write the assertions using a task. PAPER: Understanding the SVA Engine + Simple alternate solutions - SystemVerilog - Verification Academy
Abstract: Understanding the engine behind SVA provides not only a better appreciation and limitations of SVA, but in some situations provide features that cannot be simply implemented with the current definition of SVA. This paper first explains, by example, how a relatively simple assertion example can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as an error in the assertion. The paper then provides examples that uses computational variables within threads; those variables can cause, in some cases, errors in SVA. The strictly emulation model with tasks solves this issue.
hi,
I have used your above suggested code to delay using particular variable, but i am facing an issue like my assertion is getting active second time immediately where I’m not expecting and remain in active state only. Please find below code . Thanks in advance.
use above solution. However on your code you need a first_match
Antecedent |->
first_match((1, count_p7=count_p7-1’b1)[*0:$] ##1 count_p7==0)
##1 ((apcState == LD_TO_DLY) and op_signals_to_dly_p7);
Ben systemverilog.us
I am using the above solution to pass a variable latency to a property and perform checks, while trying to assert the property the tool is reporting “ERROR (EOBS012): Assert with local variable assignment in non supported position: Non negative environment.”
property perform_check(a,b,delay)
int v;
@(posedge clk) disable iff (rst)
( a , v = delay+1’b1 ) |-> (v>0, v= v-1’b1) [*0:$] ##1 v == 0 ##0 b )
endproperty
function int latency_check(a)
if ( a == some_expression )
latency_check = 3;
else
latency_check = 4
endfucntion
genvar i;
int latency
for(); begin
latency = latency_check(a);
perform_check_1 : assert property (perform_check(a,b,latency));
end