VF Horizons:PAPER: SVA Alternative for Complex Assertions

In reply to ben@SystemVerilog.us:

The main advantage of SVA is that it separates the what (the properties/sequences/etc.) from the how (the SVA engine built into the simulator). What you are advocating is clumping the two together in a big monolithic and not so readable clump. Your two leading examples for delays/repeats based on variables are written in an “inline” style. Also, no idea why you packed the code in properties and not in sequences.

Dynamic delays and repeats can’t be achieved inside the language, that’s true, but their implementation can be encapsulated in a set of helper sequences that take the number of repetitions and the expression/sequence to be repeated:



package cool_sva_utils;

  sequence variable_delay(
      int unsigned min,
      int unsigned max = min);
    // ...
  endsequence

  sequence variable_repetition(
      untyped exp_or_seq,
      int unsigned min,
      int unsigned max) = min;
    // ...
  endsequence

endpackage



import cool_sva_utils::*;

// illegal: assert property($rose(a) ##dly1 b |-> ##dly2 c);
assert property($rose(a) ##0 variable_delay(dly1) ##0 b |-> variable_delay(dly2) ##0 c);

// illegal: assert property($rose(a) |=> b[*1:max] ##1 c)'
assert property($rose(a) |=> variable_repetition(b, 0, max) ##1 c);


I’d rather see the above than a task where the entire assertion is unrolled. One could also define variants that take an infinite max number of repetitions.

Regarding assertions in classes, yes it would be nice to be able to SVA stuff inside objects, but not necessarily checks. Rather, what is more interesting is reusing SVA definitions to generate procedural code for monitors/drivers. The code writer should still specify in SVA, to achieve the nice separation of what and how.

Regarding the last example, a complex assertion, I don’t see why one would need to use ‘or’. Why can’t something like the following work:


property matching_checksum;
  <type> computed_checksum;
  $rose(go) ##0 compute_checksum(vld, data, computed_checksum) |->
      $fell(go) [->1] checksum == computed_checksum;
endproperty


sequence compute_checksum(<type> vld, <type> data, untyped computed_checksum);
  (vld[->1], computed_checksum += data) [*1:$];
endsequence

I must admit I didn’t test it. There might be some tricky cases in there, but at first glance it seems reasonable.

Even if what I wrote there doesn’t work, a little bit of support code in a checker to compute the checksum that always increments on a valid and clears on a $rose(go) is far easier to read than a task that mixes intent with execution.

If you’d have told me that you have a library of building blocks (tasks) that one can compile to emualte an SVA I would be more inclined to use it.