Assertion for ACK and REQ

SystemVerilog
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: