SVA assume/assertions for continuous data input

Question

I am an assertion based verification newbie trying to learn how it's supposed to be done properly. I have found a lot of information about the structure and technical details about the systemverilog + assertions but I still have not found somekind of a "cookbook" material of how things are really done in real world.

The question and constraints:

• Design has a data input bus with data, valid and id inputs
• One data "package" is 3 samples
• After channel n there will always be data from channel n+1
  • channel IDs will wrap after the largest ID has been sent
• There can be any number of clk ticks between data bytes

• Below is a simple and hopefully correct timing diagram with channel IDs:

  

So how do you do this with least ammount of code? Nice and clean. Previously I have build dummy verilog modules to drive the data. But surely one could just use some assume property to just constrain the channel IDs but otherwise leave free hands for the formal tool to try to brake my design?

Simple template for starters could be:

data_in : assume property (
  <data with some ID>[=3]
  |=>
  <data with the next id after any clk tick>
);

I guess the problem is that assumes/assertions like above tend to trigger on every data sample and create parallel threads which overlap in time.

Answer 1

assume property (@ (posedge clk) disable iff (rst) ((valid[->2] ##0 id != $past(id,,valid)) or ($fell(rst) ##0 valid[->1])) |=> (valid[->1] ##0 id == $past(id,,valid))[*2] ##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1));

Breaking it down: Antecedent of implication is either valid happened twice and the current id, during timestep where valid completed going high twice ([->] instead of [=]), is different from id of the last time valid went high:

((valid[->2] ##0 id != $past(id,,valid))

or valid went high immediately after rst:

($fell(rst) ##0 valid[->1])

Consequent of implication (starting one clock after antecedent matched |=> ) begins with two matches of valid going high and id == previous id (when valid was high). This MUST match twice [*].

(valid[->1] ##0 id == $past(id,,valid))[*2]

and ends with next cycle valid goes high at some point and when it does the id must be equal to previous id (when valid was high) + 1.

##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1))

This assumption allows for id to change when valid is low - but still requires that id be the same for 3 valid-high cycles.

If you want id to be stable throughout the valid times, you can use this:

assume property (@ (posedge clk) disable iff (rst) ((valid[->2] ##0 id != $past(id,,valid)) or ($fell(rst) ##0 valid[->1])) |=> ($stable(id) throughout valid[->2]) ##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1));

Answer 2

I will define three sequence to detect same id on the next valid (same_id); to detect a change of id on the next valid (change_id); and to detect a valid packet (packet_id). Then I can have one property to monitor within four valid, there are only three possible cases: ie

case1: (id, id,   id,   id+1) OR 
case2: (id, id+1, id+1, id+1) OR
case3: (id, id,   id+1, id+1) 

Please see my codes below. I haven't tested it, this is only out of my thinking. Hopefully it will work. The good thing is the property will only last for 4 clock ticks and in every clock tick, there is only one thread. So we can avoid thread explosion.

// To detect same id within two non-consecutive valid,
// (a,a)
sequence same_id;
  int prev_id;
  @(posedge clk)
  valid, prev_id=id ##1 valid[=1] ##0 id==prev_id;
endsequence


// To detect valid packet
// (a,a,a)
sequence packet_id;
  int prev_id;
  @(posedge clk)
  same_id, prev_id=id ##1 valid[=1] ##0 id==prev_id;
endsequence   

// To detect any change of ID
// any (a,b)
sequence change_id;
  int prev_id;
  @(posedge clk)
  valid, prev_id=id ##1 valid[=1] ##0 id==prev_id+1;
endsequence

// Put all together, in any four non-consecutive valid, there are only three cases: a,b,b,b OR b,b,b,c OR a,a,b,b
property next_id;
  int prev_id;
  @(posedge clk)
  (change_id ##0 packet_id) or         // a,b,b,b
  (packet_id ##0 change_id) or         // b,b,b,c
  (same_id ##0 change_id ##0 same_id); // a,a,b,b
endproperty

Answer 3

Believing that you are talking about Formal Verification Methodology.

For Formal Verification, you don't need to build any module to drive the stimulus. But instead the stimulus will be driven by the tool itself and you can guide the tool with the assume properties to generate legal stimulus.

If you don't provide any assumptions, then tool can drive any random data and evaluate the assertions, in which case, you may get false falsification. This scenario is known as "Under Constraint".

Similarly, if you provide too much assumptions, then you can miss some legal input combinations. This scenario is known as "Over Constraint".

So it is very much important, to provide exact assumptions.

For your case, your assumption may somewhat look like this :

property channel_change;
  // To check the next consecutive ID, after data transfer
  @(posedge clk)
  (id) throughout (valid [=3]) |=> valid && (id == $past(id) + 1)
endproperty

assume property (channel_change);

For more detailed information on Formal Verification Methodology, do visit my blog on that : What is Formal Verification? [1/2] & What is Formal Verification? [2/2]

Answer 4

The example you provided doesn't overlap. After three samples with the same ID, once another data sample with the next ID comes, the consequent will match and the entire property will hold.

Having overlapping attempts is anyway a fact of life. A tool always evaluates (asserted or assumed) properties in every clock cycle to figure out if a match is possible. If it decides out that it is, then it starts a new attempt; if not, it moves on. There's no way to say "don't try to consider this assertion while it's already being attempted", because you never know if an attempt will end up in a match or not.

When looking at a wave like the one you drew, it's immediately obvious that you don't need need to evaluate the property during three samples, but that's merely because you can see the whole picture. This is akin to the tool being able to see into the future.

Moving on to your concrete question, your constraint doesn't say the whole story, though. It merely states that once 3 samples with the same ID come, the ID for the next sample should be incremented. There is nothing here saying that samples must come in packets of 3. You need something like:

assume property (
  sample_with_some_id_came |->
    came_out_of_reset_and_no_samples_were_sent.triggered or
      one_or_two_samples_with_same_id_sent_after_reset.triggered or
      three_samples_with_the_previous_id_sent.triggered
);

I'm also not sure if your assume wouldn't cause some kind of "endless" behavior, since you say that there must always be a next sample after 3 samples with the same ID.