Blocking property assertion

Hi forum,

I have a property like,

function pass_action;
	Y = 1;
endtask

property some_prop;
	@(posedge clk) (X == 0) ##0 fist_match(##[1:$] (X == 1)[*2]) |-> (1, pass_action);
endproperty

I want the property to be blocking. I don’t want any other thread to start once one is started. It may start after one is finished. And don’t want to use $fell because X may start with 0 at the beginning of a simulation. What is the correct way?

I tried to use procedural expect statement,

always expect(some_prop);

But it seems like there might be a case where I don’t cover the property correctly. Which is, let’s say X is 0 and we are waiting for X to be ‘1’ for 2 cycles consecutively but it has failed at 2nd cycle after X is ‘1’. Once It has failed, I suppose it will miss the clock to start a new thread at which it failed. There will be 1 clock delay to start a new thread. Additionally, I may have something more on the consequent which consumes simulation time.

Possibly I would implement the behaviour using tasks somehow but I wonder the best approach when it comes to describing a blocking property.

One more thing, I could not find anything related to expect statement in my simulator.
Concurrent and immediate assertions are observable by default. What is your experience on expect statements related to simulators?

In reply to emin:
Quick answer now, more later when it have more time.
Check my solution on this is

One small change from my book, I would add the first_match(), as shown below.

 
module fifo_aa;
  bit clk, push, pop;
  int ticket, now_serving;
  bit [7:0] in_data, out_data;
  initial forever #5 clk=!clk;
  function void inc_ticket();
    ticket = ticket + 1'b1;
  endfunction
  property p_data_unique;
    bit [7:0] push_data;
    int v_serving_ticket;
    @(posedge clk) (push, push_data=in_data[7:0], v_serving_ticket=ticket, inc_ticket())
    |-> first_match(##[1:10] pop && now_serving==v_serving_ticket)
                                         ##0 (out_data == push_data);
  endproperty
 
  ap_data_unique: assert property(p_data_unique)
                              now_serving =now_serving+1;
                         else now_serving =now_serving+1; 

Ben Cohen

In reply to ben@SystemVerilog.us:

Thank you for a quick response Ben. I have investigated the attachments. I need to clarify that my problem is not related to the uniqueness of a thread. In your example, I understand, each push request must be followed by a pop notification, but one pop should not pass the all threads started by multiple push requests.

I desire something different. When one thread is on, I don’t want any later thread to be able to be spawned. Can you reread my post for more detail? I will try to attach a wavefrom if I can.

Also, I don’t get the use of first_match clearly. What we would expect if there is no first_match in your

property(p_data_unique)

Thanks in advance.

In reply to emin:

Also, I don’t get the use of first_match clearly. What we would expect if there is no first_match in your


|-> first_match(##[1:10] pop && now_serving==v_serving_ticket)
                                         ##0 (out_data == push_data);
/* For a constrained range (e.g., ##[1:10] you can getaway without the first_match(), 
but the error will be flagged on the 10th cycle in the above example. 
Case 1: What if in ##2 (the 10 possible ##s) pop && now_serving==v_serving_ticket)==1 but 
  (out_data is unequal push_data)? In that case, you continue the search for other ##s
   Now, what if in all the other ##s pop==0.  The assertion fails on that last 10th cycle. 
Case 2: */
|-> (##[1:$] pop && now_serving==v_serving_ticket)
                                         ##0 (out_data == push_data);
/* What if in ##2 (the 10 possible ##s) pop && now_serving==v_serving_ticket)==1 but 
  (out_data is unequal push_data)? In that case, you continue the search for other ##s
   Now, what if in all the other ##s pop==0.  The assertion NEVER fails. 
   You lost the opportunity to check it when pop && now_serving==v_serving_ticket)was ==1
   at cycle 2. */ 

On the other question on uniqueness, see below (it is lengthy).


/* First-come/First-served, First-come/NO-others/Next-First-come, Expect. 
* Since every successful attempt at an assertion initiate its own consequent, 
if multiple concurrent assertions are in the active state waiting for a successful 
consequent, any successful consequent with complete ALL of the pending assertions. 
For example: @(posedge clk) $rose(req) |-> ##[1:10]   ack; 

* There are cases though when the requirements are searching for uniqueness, 
  and there are two possibilities for uniqueness: 
  - First-come/First-served and 
  - First-come/NO-others/Next-First-come

  In a first-come puts all other-comes as recognized, but put into a waiting queue 
  to be served in that order when each first-come is finished with the transaction 
  (with a pass or a fail).   
  To accomplish this, one could use concepts of a familiar model seen in hardware stores 
  in the paint department. There, the store provides a spool of tickets, each with a number. 
  As a customer comes in, he takes a ticket. The clerk serving the customers has a sign that reads 
  "NOW SERVING, TICKET #X". The customer that has the ticket gets served, 
  the others have to wait. When done, the number X in incremented, 
  and the next in-line customer gets served.  Here is a model for that: */  
module top; 
    import uvm_pkg::*; `include "uvm_macros.svh" 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk,req, ack;  
    int ticket, now_serving; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    function void inc_ticket(); 
        ticket = ticket + 1'b1; 
    endfunction 

    property reqack_unique;
        int v_serving_ticket;
        @(posedge clk) ($rose(req),  v_serving_ticket=ticket, inc_ticket()) |-> 
             first_match(##[1:10] now_serving==v_serving_ticket) ##0 ack; 
    endproperty
    ap_reqack_unique: assert property(reqack_unique) 
         now_serving =now_serving+1; else now_serving =now_serving+1; 
    
    
    initial begin 
        repeat(100) begin 
            @(posedge clk); #1;  
            if (!randomize(req, ack)  with 
            { req dist {1'b1:=1, 1'b0:=3};
            ack dist {1'b1:=1, 1'b0:=5};       
        }) `uvm_error("MYERR", "This is a randomize error")
    end 
    repeat(200) begin
        @(posedge clk); #1
        if (!randomize(req, ack)  with 
        { req dist {1'b1:=1, 1'b0:=3};
        ack dist {1'b1:=0, 1'b0:=1};       
    }) `uvm_error("MYERR", "This is a randomize error")
    end
    $stop; 
   end 
endmodule   
/* First-come/NO-others/Next-First-come
 In this model, after a first-come the door is closed and all other-comes are not recognized. 
 When that first-come is done (pass or fail), the next first-come is accepted and the door is closed again. 
 
 To accomplish this, one could use concepts of a familiar model seen in a 
 store that only has a ONE-SPACE parking spot.  If the spot is empty, a customer can park 
 and go to the store.  If the spot is full, any new comer MUST leave because regulations do not allow
 parking waiting for the spot; he can go around the block if he wants, but when he comes 
 back it is considered a new arrival. 

 The implemntation is similar to the previous model, but uses a lock/unlock. If lock is ON, 
 any new attempt beccomes vacuous.  Below is a model: */
 
module top; 
    import uvm_pkg::*; `include "uvm_macros.svh" 
    timeunit 1ns;     timeprecision 100ps;  
    typedef enum {UNLOCKED, LOCKED} lock_enum;  
    bit clk,req, ack;  
    lock_enum lock=UNLOCKED; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    function void lock_fnct(lock_enum x); 
        lock = x; 
    endfunction 

    property reqack_unique;
        int v_serving_lock;
        @(posedge clk) ($rose(req) && lock==UNLOCKED,  lock_fnct(LOCKED)) |-> 
                                     ##[1:10]  (ack, lock_fnct(UNLOCKED)); 
    endproperty
    ap_reqack_unique: assert property(reqack_unique) else lock_fnct(UNLOCKED);  
    
    initial begin 
        repeat(100) begin 
            @(posedge clk); #1;  
            if (!randomize(req, ack)  with 
            { req dist {1'b1:=1, 1'b0:=3};
            ack dist {1'b1:=1, 1'b0:=5};       
        }) `uvm_error("MYERR", "This is a randomize error")
        end 
    repeat(200) begin
        @(posedge clk); #1
        if (!randomize(req, ack)  with 
        { req dist {1'b1:=1, 1'b0:=3};
        ack dist {1'b1:=0, 1'b0:=1};       
    }) `uvm_error("MYERR", "This is a randomize error")
        end
        $stop; 
    end 
endmodule   

/* What about the "expect" construct to achieve uniqueness. 
The expect construct is not part of the “verification layer” because it does not make a statement 
about what should be done with a property in terms of verification. However, the expect statement 
makes use of a property. Specifically,  the expect statement can appear anywhere a wait statement 
can appear (e.g., always procedure, task (but not in classes!!!)). The expect statement is a procedural 
blocking statement that allows waiting on a property evaluation. 
The expect statement accepts the same syntax used to assert a property. 
   expect_property_statement ::= expect ( property_spec ) action_block
An expect statement causes the executing process to block until the given property succeeds or fails. 
The statement following the expect is scheduled to execute after processing the Observed region 
in which the property completes its evaluation.
When the property succeeds or fails, the process unblocks, and the property stops being evaluated 
(i.e., no property evaluation is started until that expect statement is executed again). 
<<< -- When executed, the expect statement starts a single thread of evaluation for the given property
on the subsequent clocking event, that is, the first evaluation shall take place on the next clocking event. -->>
If the property fails at its clocking event, the optional else clause of the action block is executed. 
If the property succeeds, the optional pass statement of the action block is executed. 
The execution of pass and fail statements can be controlled by using assertion action control tasks 
The model below works like the unique-lock, but the simulator reports no statistis or 
waveform or debug features. : */

module top; 
    import uvm_pkg::*; `include "uvm_macros.svh" 
    timeunit 1ns;     timeprecision 100ps;  
    typedef enum {UNLOCKED, LOCKED} lock_enum;  
    bit clk,req, ack;  
    lock_enum lock=UNLOCKED; 
    event pass, fail; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    function void lock_fnct(lock_enum x); 
        lock = x; 
    endfunction 

    property reqack_unique;
        int v_serving_lock;
        @(posedge clk) ($rose(req) && lock==UNLOCKED,  lock_fnct(LOCKED)) |-> 
                                     ##[1:10]  (ack, lock_fnct(UNLOCKED)); 
    endproperty
    ap_reqack_unique: assert property(reqack_unique) else lock_fnct(UNLOCKED);  

    property reqack_expect;
        int v_serving_lock;
        @(posedge clk) $rose(req)  |-> ##[1:10]  ack; 
    endproperty
    always 
       expect (reqack_expect) -> pass; else -> fail;
    
    initial begin 
        repeat(100) begin 
            @(posedge clk); #1;  
            if (!randomize(req, ack)  with 
            { req dist {1'b1:=1, 1'b0:=3};
            ack dist {1'b1:=1, 1'b0:=5};       
        }) `uvm_error("MYERR", "This is a randomize error")
        end 
    repeat(200) begin
        @(posedge clk); #1
        if (!randomize(req, ack)  with 
        { req dist {1'b1:=1, 1'b0:=3};
        ack dist {1'b1:=0, 1'b0:=1};       
    }) `uvm_error("MYERR", "This is a randomize error")
        end
        $stop; 
    end 
endmodule   

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

In reply to ben@SystemVerilog.us:

In reply to emin:


|-> first_match(##[1:10] pop && now_serving==v_serving_ticket)
##0 (out_data == push_data);
/* For a constrained range (e.g., ##[1:10] you can getaway without the first_match(), 
but the error will be flagged on the 10th cycle in the above example. 
Case 1: What if in ##2 (the 10 possible ##s) pop && now_serving==v_serving_ticket)==1 but 
(out_data is unequal push_data)? In that case, you continue the search for other ##s
Now, what if in all the other ##s pop==0.  The assertion fails on that last 10th cycle. 
Case 2: */
|-> (##[1:$] pop && now_serving==v_serving_ticket)
##0 (out_data == push_data);
/* What if in ##2 (the 10 possible ##s) pop && now_serving==v_serving_ticket)==1 but 
(out_data is unequal push_data)? In that case, you continue the search for other ##s
Now, what if in all the other ##s pop==0.  The assertion NEVER fails. 
You lost the opportunity to check it when pop && now_serving==v_serving_ticket)was ==1
at cycle 2. */ 

So in case 2, we let it fail once pop && now_serving==v_serving_ticket is satisfied if out_data is unequal to push_data. Because otherwise simulator is thinking like there would be another match of the sequence tied to unbounded delay.

I want to add,

In this property,

property some_prop;
	@(posedge clk) $fell(X) ##0 (##[1:$] (X == 1)[*2]) |-> ##2 (1, pass_action);
endproperty

I observed that once $fell(X) is satisfied, a new thread is spawned looking for the later sequence to match. But even though antecedent is matched for the first time, I saw the second antecedent match in the next clock in the same thread (2 antecedent matches consecutively). But I would expect that antecedent is already matched and just move on to consequent. After adding,

first_match to (##[1:$] (X == 1)[*2])

problem is solved.
What is going on behind the scenes really?

In reply to emin:

You’re correct on all; you can apply the first_match() on the whole antecedent.
I strongly recommend that you read my paper that also addresses the multithreading in antecedents. Understanding the model using tasks will give you a better appreciation of SVA and will make you a better coder because you’ll have a deeper understanding of the inner works (though the actual implementation of SVA is different).
Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

In reply to ben@SystemVerilog.us:
One more comment: MAny experts on SVA frown upon the use of the first_match() from a style point of view and prefer to use the goto operator if possible. Thus, you could write the following:


// Instead of 
@(posedge clk) $fell(X) ##0 (##[1:$] (X == 1)[*2]) |-> ##2 (1, pass_action);

// Write
@(posedge clk) $fell(X) ##0 X==1[->1] ##1 X==1 |-> ##2 (1, pass_action);

Ben SystemVerilog.us

In reply to ben@SystemVerilog.us:

On the other question on uniqueness, see below (it is lengthy).

I think I have completely understood the behaviour in 3 examples except,

“it does not make a statement about what should be done with a property in terms of verification.”

Can you elaborate what you really mean here?
I will try to fit my requirement and will post here again based on my experience. Thank you really.

In reply to ben@SystemVerilog.us:

In reply to emin:
I strongly recommend that you read my paper that also addresses the multithreading in antecedents. Understanding the model using tasks will give you a better appreciation of SVA and will make you a better coder because you’ll have a deeper understanding of the inner works (though the actual implementation of SVA is different).

I will definetely read it as its already in my list :))

In reply to ben@SystemVerilog.us:

In reply to ben@SystemVerilog.us:
One more comment: MAny experts on SVA frown upon the use of the first_match() from a style point of view and prefer to use the goto operator if possible. Thus, you could write the following:


// Instead of 
@(posedge clk) $fell(X) ##0 (##[1:$] (X == 1)[*2]) |-> ##2 (1, pass_action);
// Write
@(posedge clk) $fell(X) ##0 X==1[->1] ##1 X==1 |-> ##2 (1, pass_action);

Ben SystemVerilog.us

This does not seem to me the same. With first_match, I doubt it won’t fail even after X==1 ##1 X==0 happens, it will be looking for the next matches without failing. But here I expect that it will fail since X==1[->1] is satisfied and we force it to be X==1; thread dies if X==0. Hence, we will need another fell of X to be started.
And what if we have more complicated sequence than (X == 1)[*2]?

In reply to emin:

In reply to ben@SystemVerilog.us:
This does not seem to me the same. With first_match, I doubt it won’t fail even after X==1 ##1 X==0 happens, it will be looking for the next matches without failing. But here I expect that it will fail since X==1[->1] is satisfied and we force it to be X==1; thread dies if X==0. Hence, we will need another fell of X to be started.
And what if we have more complicated sequence than (X == 1)[*2]?

Ok, I think I failed :). New thread will already be spawned since its concurrent.

In reply to emin:

The expect:“it does not make a statement about what should be done with a property in terms of verification.”
Can you elaborate on what you really mean here?

The expect construct is not part of the “verification layer” in that it is not an assertion, or a cover or an assume but more of a block that executes the property **starting from the next clocking event
** (e.g., the next @(posedge clk)). The expect is not processed by the simulator as an assertion; thus, there is NO statistics as to PASS/FAIL of that property, NO wave view of the activities. Also, there is no internal debug of that property. Some simulators have in debug mode thread viewing capabilities.
To really understand the expect I created this trivial model. I annotated the timing results. The bottom line, if you use the expectconstruct, you must really understand its implications in terms of timing (the blocking and starting at next clocking event) and the lack of verification support by the tool. You are responsible to keep track of the statistics. The expectblocking ends when the property completes, pass or fail.
For reference, model http://systemverilog.us/vf/play.sv
Timing : http://systemverilog.us/vf/the_expect_eval.png


module top;
  bit clk=1, a, b, reset_n;
  event e0, e1, e2, e_expt, e3, e4;
  initial forever #10 clk = !clk;
  function void setevent();
      -> e_expt;
  endfunction
  always @(posedge clk) begin
      int az;
      az=2;
      -> e0;
      ap_inalways: assert property(@ (posedge clk) 1 |-> ##1 1 ) -> e1;  
      ap_var_a: assert property(@ (posedge clk) az==2 |-> ##1 1 ) -> e2;  
      expect(@ (posedge clk) (1, setevent()) |-> ##1 1) -> e3; else -> e4; 
  end
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

In reply to ben@SystemVerilog.us:

This is definitely what I wanted! I understood the concept broadly. Thank you for your great attention, I appreciate it Ben.

In reply to emin:
Found out that the **expect** is a leftover from a pre-SVA construct in Vera and its syntax was merged with the property specification. It is very rarely used except maybe in translating Vera code to SystemVerilog.
Ben