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: