Assertion: Valid should fall within 13 clock cycles until Req is high

SystemVerilog
, , , ,
1

Hi ,

I need two types of assertions

  1. When req raises and when valid is 1, within 13 clock cycle valid should fall until req is 1.
   property (req,valid);
    @(Clk)
    ($rose(req) valid)|->##[0:13] $fell(valid) throughout (req[->1]);
   endproperty

I am getting this error
A temporal LHS is not allowed with the ‘throughout’ operator.
Expression: ##[0:13] $fell(valid)) throughout (req [-> 1])

  1. When Req raises, after 12 clock cycles, vaild should not raise until Req is 1.
   property prop_req(req,valid);
    @(Clk) 
    ($rose(req) ##1 req[*12] ) |-> !$rose(valid) throughout (~req[->1]);
  endproperty

Is my above assertion correct?

2

In reply to naaj_ila:
within 13 clock cycle valid should fall until req is 1.
YOUR requirements are not clear. 2 options depending on what you want


    ($rose(req)&& valid)|->
        (##[0:13] $fell(valid)) intersect (req[->1]);
 ($rose(req)&& valid)|->
        (##[0:13] $fell(valid)) and (req[->1]); // propably this 

// When Req raises, after 12 clock cycles, vaild should not raise until Req is 1 
//($rose(req) ##1 req[*12] ) |-> !$rose(valid) throughout (~req[->1]);
 // that does express the requirements
// also, I don't understand your requirements 
You need to rewrite them. 
You wrote a rose of req, followed by a repeat of req 12 times as an antecedent. 
The consequent has no rose of valid throughout req[*0:$] ##1 !req

Ben Ben@systemverilog.us

3

Hi Ben, Thanks for the reply.
Here is the flow.
Assertion1)

  1. When Req raises, Valid can rise within 13 clock cycle
  2. After 13 clock cycles, Valid should not rise during Req=1.
    (If Req drops after 13 clock cycle, should not check Valid)

Assertion2)

  1. When Req raises and when Ready is 1.
    Valid should drop within 13 clock cycles during Req=1.
    (If Req drops within 13 clock cycle, should not check Valid)
4

In reply to naaj_ila:
Hope this will help you in the right direction. Again, you need to understand the sequence and property operators.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
	bit clk, req, valid, ready;  
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    /* Assertion1)
    1. When Req raises, Valid can (or must? rise within 13 clock cycle
    2. After 13 clock cycles, Valid should not rise during Req=1. */
    ap_reqvld_must: assert property(  // Valid MUST rise
      $rose(req) |->  
         ##[1:13] $rose(valid) ##1 !valid throughout req[*1:$] ##1 $fell(req));
    
    ap_reqvld_can: assert property(  // Valid can rise
       first_match($rose(req)  ##[1:13] $rose(valid))|->  
          ##1 !valid throughout req[*1:$] ##1 $fell(req));
    
    /* Assertion2)
    1. When Req raises and when Ready is 1.
    Valid should drop within 13 clock cycles during Req=1.
    (If Req drops within 13 clock cycle, should not check Valid) */
    ap_reqready: assert property(  
    $rose(req) ##0 ready[->1]|->
    (##[0:13] $fell(valid)) intersect req[->1]); //   No check for req drop 

    ap_reqready_reqdrop: assert property(  
    $rose(req) ##0 ready[->1]|->
    (##[0:13] $fell(valid)) intersect req[->1]) or 
     (##[0:13] $fell(req)); //  passes if req drops 
    
    initial begin 
        repeat(200) begin 
            @(posedge clk);   
            if (!randomize(req, valid, ready)  with 
            { req   dist {1'b1:=1, 1'b0:=3};
            valid dist {1'b1:=1, 1'b0:=6};
            ready dist {1'b1:=1, 1'b0:=6};      
        }) `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 Home - My cvcblr

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy