SVA - Sequence doubt

Currently I have an sequence in which I am trying to track the sequence of values that change in the signal over a period of time:


property sel_dac (vsrc,  vsrc_exp);
@(posedge clk2)
	$rose(algo_start) |-> (vsrc == 0)[*1:$] ##1  **(vsrc==vsrc_exp)** [*1:$] ##1 ((vsrc==0) throughout $fell(algo_start)[->1]);
endproperty

This seems to work in most of the cases. vsrc_exp is calculated based on some other values.

Issue is the vsrc(design value) sometimes changes after a few clock cycles but the vsrc_exp(expected value) is already calculated.

ex: vsrc = 2.3 at 100 ns, 2.7 at 120 ns, 2.9 at 140 ns which is absolutely fine!
and vexp = 2.3 at 100 ns, 2.7 at 110 ns, 2.9 at 140 ns which is also fine!

I want the sequence to be able to wait for this change which could sometime take around 10 cycles. One way to address is to write

(vsrc==vsrc_exp) ##[1:10]

,

(vsrc==vsrc_exp) ##[1:$]

But, I don’t want to hardcode numbers as it would take away the flexibility and will be hard to keep track
Also, ##[1:$] would just ignore every other change that happens (ex: if vsrc goes to 5 which is wrong) and make the sequence useless.

Please let me know if there are better ways to solve this issue. Thanks for the help.

In reply to bharath_1800:
I struggled through your requirements. In your property

property sel_dac (vsrc,  vsrc_exp);
@(posedge clk2)
	$rose(algo_start) |-> (vsrc == 0)[*1:$] ##1  [(vsrc==vsrc_exp) [*1:$] ##1 ((vsrc==0) throughout $fell(algo_start)[->1]);
endproperty  

You’re stating:

  1. Upon a start of the algorithm
  2. vsrc (the result) is 0 for a while until
  3. the result sequence is same as the expected sequence
  4. and the last value of that expected is 0.
  5. The end of the sequence occurs when the envelope of the start of the algorith falls.

What you have as a property should do that. I am missing your issues.
Consider rewriting your requirements with tasks and automatic task variables, as explained in my paper at PAPER: Understanding the SVA Engine + Simple alternate solutions | Verification Academy
The tasks will give you greater flexibility in doing exactly what you want. Keep in my that an assertion defines the properties that a design must meet; it can be done in SVA or with just plain code. My paper emulates SVA with tasks, and that gives you a lot more flexibility. Explain your requirements.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


In reply to ben@SystemVerilog.us:

Hi Ben! You’re right on the problem statement.

I will explain my issue in more detail now:
“vsrc (the result) is 0 for a while until the result sequence is same as the expected sequence”

Here the issue I am observing is, result sequence and expected sequence values don’t change at the same time. What is happening is that the result changes its value 2 or 3 cycles later than the expected value and the SVA shouldn’t trigger false for this.

ex: vsrc = 2.3 at 100 ns, 2.3 at 110ns, 2.7 at 120 ns, 2.9 at 140 ns which is absolutely fine!
and vexp = 2.3 at 100 ns, 2.7 at 110ns, 2.7 at 120 ns, 2.9 at 140 ns which is also fine!

After vsrc = 0 changes to vsrc=vexp=2.3, I am expecting the sequence (vsrc==vsrc_exp) to keep track of all the changes happening i.e 2.3 to 2.7 to 2.9

Hope that gives better idea of the issue.

In reply to bharath_1800:

What is happening is that the result changes its value 2 or 3 cycles later than the expected value and the SVA shouldn’t trigger false for this.

  1. If the delay is fixed and known, then delay the expected sequence by the amount using supporting logic (i.e., a shift reg), and take the delayed values as the expected. Essentially, doing a sync.
  2. If the delay is not fixed, then you can do something like the following

// Reference my paper too.
property sel_dac (vsrc,  vsrc_exp);
@(posedge clk2)
$rose(algo_start) |-> (1, check_t());
endproperty
task automatic check_t(); // // syntax not checked, + pseudo code
automatic in_srcQ, expected_Q;
// vsrc == 0)[*1:$] ##1  [(vsrc==vsrc_exp) [*1:$] ##1 ((vsrc==0) throughout $fell(algo_start)[->1]);
while (!$fell(algo_start)) begin
@(posedge clk2);
put_in_src_Q(expected_value);
put_in_result_Q(result_value);
end
// If here, all data needed is stored in 2 Queues
// Now loop thru the queues, sync up to the 1st non-zero result and compare
// in a simple loop (with no clocks)
// if error, assert(0)
endtask
// (vsrc == 0)[*1:$] ##1  [(vsrc==vsrc_exp) [*1:$] ##1 ((vsrc==0) throughout $fell(algo_start)[->1]);

I’ll let you do the coding, but that is the approach; basically storing the 2 values (expected and actuals), and when done storing, do a loop by syncing the expected against actual with the non-zeros, and then compare.
Ben Ben@systemverilog.us