PSL assertion for variable delay pipeline

Question

I am trying to write a PSL assertion that checks that the amount of assertions on the input match the amount of assertions on the output.

For example:

.

On the input anything can happen at any time and the output can be asserted on any time as well. The exact time is unknown and also not important. What I want to verify is that no information is dropped.

I've come up with the following PSL statement to verify this. This is a strong assertion meaning that at the end of a test all assertions need to have been "completed".

assert always { input='1' |-> {[*] ; output='1'} }!;

For example, the following should be a failure but this PSL passes:

I noticed that this statement is not strong because different input assertions can be matched by the same output assertion. For example:

What would be a good way of implementing a PSL like this? Obviously I can also verify it through other means (counting input and output assertions) but would there be a way to do this with PSL? Is there an equivalent check that I could implement using SVA?

Input was asserted for two cycles ("2 transactions") but the output is only asserted for 1 cycle. In this case that implies that a transaction was "dropped". But yes, maybe I did not wait long enough. I will add an explanation that the assertions are strong and that at the end of simulation all PSL assertions need to have been completed. — Maurice, Jun 04 '20 at 17:18

score 0 · Answer 1 · answered Jul 01 '20 at 20:07

I may be missing something here, but why not simply implement counters and compare them at end of test?

always @(posedge clk) bgein
  if (reset) begin
    counter_in <= 0;
    counter_out <= 0;
  end else begin
    if (input_) counter_in++;
    if (output_) counter_out++;
  end
end 
final begin
  assert (counter_in == counter_out);
end

even if you get overflow it would still work.

PSL assertion for variable delay pipeline

1 Answers1