Task Used In Property of Assertions

SystemVerilog
, ,
1

I’m not familiar with the syntax below. I tried to search online but I couldn’t find an answer. This is a task used inside a property of the assertion. May I know what (1, my_task()) means?


property my_property(logic clk, logic a, logic b);
  @(posedge clk)
  a |-> (1, my_task(b));
endproperty
2

In reply to Reuben:

I’m not familiar with the syntax below. I tried to search online but I couldn’t find an answer. This is a task used inside a property of the assertion. May I know what (1, my_task()) means?


property my_property(logic clk, logic a, logic b);
@(posedge clk)
a |-> (1, my_task(b));
endproperty

(1, my_task(b)) is a one of the option of a sequence; the “my_task(b)” is called the sequence_match_item.

sequence_expr ::= …
| ( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ]
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
| subroutine_call


// consider the following 
bit w;
ap: assert property(@(posedge clk)  a |-> (w, my_task(b))); 
// This says that if(a) then if(w==1) do the my_task call.
// *** Now, if you always want to do the task call in the consequent, 
// then replace the  "w" with 1. 
ap: assert property(@(posedge clk)  a |-> (1, my_task(b)));

See 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.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

3

In reply to ben@SystemVerilog.us:

Hi Ben. Thanks for the clarification. I have another question. In order for that assertion to be true, how will the my_task(b) defines it? The consequent only has the my_task(b) so I don’t know how the assertion will be evaluated as true or false. Does it only need to finish the task then it will evaluate the assertion as true?

4

In reply to Reuben:
You’re correct in that, unlike a function call, the task returns nothing.
Keep in mind that the goal of an assertion is to determine is a property is true or false.
That true/false flag need not necessarily come from the assertion statement; it can come from the task. In my paper, I show the following example where I demonstrate the use of uvm_error. You can also use instead of the uvm_error an immediate assertion.
If the task has no clocking statements, use a function, as shown below.

function automatic logic do_this(bit a); 
  automatic int v; 
  v = a || e ; 
  return v; 
endfunction : do_this  
property p; 
  bit w, r; 
  (a, w=q) |=> (1, r=do_this(w)) ##0 r; // r get the result of the function call
  // if r==0, the property is false and the assertion fails. 
endproperty

Using tasks // from http://systemverilog.us/vf/understanding_assertions.pdf


// emulating: 
ap_ab_then_c : assert property($rose(a) ##2 b |-> ##3 c); 

task automatic t_ab_then_c();
 if($rose(a)) begin : rose_a // attempt succeeds
 repeat(2) @(posedge clk);
 if(b) begin : got_b // antecedent match
repeat(3) @(posedge clk);
if(c) // consequent match
 `uvm_info (tID,$sformatf("%m : AB_then_C PASS, c= %b", c), UVM_HIGH)
else // consequent does not match
 `uvm_error(tID,$sformatf("%m : AB_then_C FAIL @ c= %b", c))
 end : got_b
 else return; // vacuous pass, antecedent does not match
 end : rose_a
endtask

// ALSO OK 
task automatic t_c();
  // antecedent match
  repeat(3) @(posedge clk);
  if(c) // consequent match
  `uvm_info (tID,$sformatf("%m : AB_then_C PASS, c= %b", c), UVM_HIGH)
  else // consequent does not match
   `uvm_error(tID,$sformatf("%m : AB_then_C FAIL @ c= %b", c))
endtask
ap_ab_then_c2 : assert property($rose(a) ##2 b |-> (1, t_c());

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr