Assertion for ACK and REQ

SystemVerilog
1

Hi,

Assertion has to be coded for the following scenario.

  1. once the req come on the posedge of the clock, the ack should occur within 10 to 20 clock cycles.
  2. second req should not occur until the ack for first request is completed.

Please let me know on this.

Thanks
STA

2

In reply to syed taahir ahmed:

Add a variable “bit busy;”
Upon a successful req, call a function to set busy=1. At the conclusion of the assertion, pass or fail, reset the busy.

Write a 2nd assertion “not (req && busy);”
Given those guidelines, write the assertion.
Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Hi Ben,

I couldn’t understand the second assertion part.

The req will be high for one clock and then ack should occur within 10 to 20 cycles. Req should not occur until the ack completed.

Thanks

4

Ben,

I guess the following assertion would cover both the requirements :

property req_ack;
@(posedge refclk)
$rose(req) |=> (##[9:20] ack) intersect (!req throughout ack[->1]);
endproperty

Thanks

5

In reply to sjain12:

Good solution, I like it!
Ben systemverilog.us

6

In reply to sjain12:

Thanks Jain for your reply,

7

In reply to manjutumn:

  1. The assertion would still fail if the request is not a single cycle pulse.
  1. second req should not occur until the ack for first request is completed.

You need to add another assertion to cover the needed cases. Edit the code below to meet your requirements. I am providing concepts here.


// on item 1) I don't quite understand it.  Do you mean
ap_no2req: assert property(
not(req[*2]); 
// On item 2)
// Add a variable "bit busy;"
// Upon a successful req, call a function to set busy=1. 
// At the conclusion of the assertion, pass or fail, reset the busy.
// Write a 2nd assertion "not (req && busy);"
/*second req should not occur until the ack for first request is completed.[/quote]
You need to add another assertion to cover the needed cases.   */
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
bit clk,req, ack, busy;
initial forever #10 clk=!clk;

function void setbusy(bit x);
    busy=x;
endfunction

ap_set_busy: assert property(@ (posedge clk)
                             ($rose(req) && !busy, setbusy(1)) |-> ack[->1] ##0 (1, setbusy(0)))
else setbusy(0);

    ap_no_2nd_req_until_ack: assert property(@ (posedge clk)
            not(req && busy));

initial begin
    bit va, vb;
    repeat(200) begin
        @(posedge clk);
        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
    $stop;
end
endmodule

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

** 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:
8

In reply to manjutumn:

  1. The assertion would still fail if the request is not a single cycle pulse.
  1. second req should not occur until the ack for first request is completed.

You need to add another assertion to cover the needed cases.


// on item 1) I don't quite understand it.  Do you mean
ap_no2req: assert property(
not(req[*2]); 
// On item 2)
// Add a variable "bit busy;"
// Upon a successful req, call a function to set busy=1. 
// At the conclusion of the assertion, pass or fail, reset the busy.
// Write a 2nd assertion "not (req && busy);"
/*second req should not occur until the ack for first request is completed.[/quote]
You need to add another assertion to cover the needed cases.   */
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
bit clk,req, ack, busy;
initial forever #10 clk=!clk;

function void setbusy(bit x);
    busy=x;
endfunction

ap_set_busy: assert property(@ (posedge clk)
                             ($rose(req) && !busy, setbusy(1)) |-> ack[->1] ##0 (1, setbusy(0)))
else setbusy(0);

    ap_no_2nd_req_until_ack: assert property(@ (posedge clk)
            not(req && busy));

initial begin
    bit va, vb;
    repeat(200) begin
        @(posedge clk);
        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
    $stop;
end
endmodule

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

** 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:
9

Hi @ben2
Can you please this

property req_ack;
  @(posedge refclk)
  $rose(req) |=> (##[9:20] ack) intersect (!req throughout ack[->1]);
endproperty
10

By that, do you mean something like:
upon a new req, starting from the next cycle req==0 and ack==0 for 8 cycles.
following this sequence, req==0 until ack that shall occur with the next 12 cycles

 $rose(req) |=> !req && !ack[*1:8] ##1
                          (ack[->1] intersect !req[*12]) ;
11

I would write properties like the followings.

//          _ 1 3 3   10        20
// req : __| |_____   ____
//                     <---_--->
// ack :    _______   ____|

property req_ack;
  $rose(req) |-> !ack ##1 (!req&&!ack)[*9:19] ##1 $rose(ack);
endproperty

or

property req_low_until_ack;
  $rose(req) |=> !req[*10:20] ##0 $rose(ack);
endproperty

property ack_low;
  $rose(req) |-> !ack[*10];
endproperty
12

Hi Ben,
I was wondering if @sjain12’s solution can be rewritten as

property req_ack;
  @(posedge refclk)
    $rose(req) |=> (##[9:20] ack) and  (!req throughout ack[->1]);
endproperty

Thanks

13

Looks good.
On a related topic, see my paper
The Traditional Req/Ack Handshake, It’s More Complicated Than You Think!