Avoiding support code for SVA sequence to handle pipelined transaction

Question

Let's say we have a protocol that says the following. Once the master sets req to fill, the slave will signal 4 transfers via rsp:

An SVA sequence for this entire transaction would be (assuming that the slave can insert idle cycles between the trans cycles):

req == fill ##1 (trans [->1]) [*4];

Now, assume that the master is allowed to pipeline requests. This would mean that the next fill is allowed to start before the 4 trans cycles are done:

The SVA sequence from above won't help, because for the second fill it's going to wrongly match 4 trans cycles, leaving the last trans "floating". It would need to start matching trans cycles only after the ones for the previous fill have been matched.

The sequence needs global information not available in a single evaluation. Basically it needs to know that another instance of it is running. The only way I can think of implementing this is using some RTL support code:

int num_trans_seen;
bit trans_ongoing;
bit trans_done;
bit trans_queued;

always @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    num_trans_seen;
    trans_ongoing <= 0;
    trans_done <= 0;
    trans_queued <= 0;
  end
  else begin
    if (trans_ongoing)
      if (num_trans_seen == 3 && req == trans) begin
        trans_done <= 1;
        if (req == fill || trans_queued)
          trans_queued <= 0;
        else
          trans_ongoing <= 0;
        num_trans_seen == 0;
      end
    else
      if (trans_queued) begin
        trans_queued <= 0;
        trans_ongoing <= 1;
      end

    if (trans_done)
      trans_done <= 0;
  end

The code above should raise the trans_ongoing bit while a transaction is ongoing and pulse trans_done in the clock cycle when the last trans for a fill is sent. (I say should because I didn't test it, but this isn't the point. Let's assume that it works.)

Having something like this, one could rewrite the sequence to be:

req == fill ##0 (trans_ongoing ##0 trans_done [->1]) [*0:1]
  ##1 (trans [->1]) [*4];

This should work, but I'm not particularly thrilled about the fact that I need the support code. There is a lot of redundancy in it, because I basically re-described a good chunk of what a transaction is and how pipelining works. It's also not as easily reusable. A sequence can be placed in a package and imported somewhere else. The support code can only be placed in some module and reused, but it's a different logical entity than the package that would store the sequence.

The question here is: is there any way to write the pipelined version of the sequence while avoiding the need for support code?

Answer 1

It looks like rsp is always idle before the trans starts. If rsp's idle is a constant value and it is a value that trans will never be, then you could use:

req == fill ##0 (rsp==idle)[->1] ##1 trans[*4];

The above should work when the pipeline supports 1 to 3 stages.

For a 4+ deep pipeline, I think you need some auxiliary code. The success/fail blocks of the assertion can be used to incompetent the count of completed trans; this saves you from having write additional RTL. A local variable in the property can be used to sample the fill's count value. The sampled value will be used as a criteria to start sampling the expected trans pattern.

int fill_req;
int trans_rsp;
always @(posedge clk, negedge rst_n) begin
  if(!rst_n) begin
    fill_req <= '0;
    trans_rsp <= '0;
  end
  else begin
    if(req == fill) begin
      fill_req <= fill_req + 1; // Non-blocking to prevent risk of race condition
    end
  end
end

property fill_trans();
  int id;
  @(posedge clk) disable iff(!rst_n)
  (req == fill, id = fill_req) |-> (rsp==idle && id==trans_rsp)[->1] ##1 trans[*4];
endproperty

assert property (fill_trans()) begin
  // SUCCESS
  trans_rsp <= trans_rsp + 1; // Non-blocking to prevent risk of race condition
end
else begin
  // FAIL
  // trans_rsp <= trans_rsp + 1; // Optional for supporting pass after fail
  $error("...");
end

FYI: I haven't had time to fully test this. It should at least get you in the right direction.

---

---

I experimented a bit more and found a solution that might be more to your liking; no support code.

The equivalent of trans[->4] is (!trans[*] ##1 trans)[*4] per IEEE Std 1800-2012 § 16.9.2 Repetition in sequences. Therefore we can use the local variables to detect new fill requests with the expanded form. For example the following sequence

sequence fill_trans;
  int cnt;                                // local variable
  @(posedge clk)
  (req==FILL,cnt=4) ##1 (                 // initial request set to 4
    (rsp!=TRANS,cnt+=4*(req==FILL))[*]    // add 4 if new request
    ##1 (rsp==TRANS,cnt+=4*(req==FILL)-1) // add 4 if new request, always minus 1
  )[*] ##1 (cnt==0);                      // sequence ends when cnt is zero
endsequence

Unless there is another qualifier not mentioned, you cannot use a typical assert property(); because it will start new assertion threads each time there is a fill request. Instead use an expect statement, which allows waiting on property evaluations (IEEE Std 1800-2012 § 16.17 Expect statement).

always @(posedge clk) begin
  if(req==FILL) begin
    expect(fill_trans);
  end
end

I tried recreating your describe behavior for testing https://www.edaplayground.com/x/5QLs