Multiple Clock Assertion in Systemverilog

Question

Here is the Design Code :

module mul_clock (input clkA, clkB, in, output out);
  bit temp;
  reg x[2:0];

  always @ (posedge clkA)
    temp <= temp ^ in;

  always @ (posedge clkB)
    x <= {x[1:0], temp};

  assign out = x[2] ^ x[1];
endmodule

How to write Assertion for "Out", as it is a multi-clock design.

I have tried one, but still getting some errors. Kindly help me to modify this assertion or to write another one :

property p1;
  bit t;
  bit x[2:0];

  @(posedge clkA)
  (1'b1, t ^= in) |=> @(posedge clkB) (1'b1, x[0] = t) |=> @(posedge clkB) (out == x[2] ^ x[1], x[1] = x[0]) |=> @(posedge clkB) (out == x[2] ^ x[1], x[2] = x[1]);
endproperty

Note : With always block and a single clock assertion, we can verify out port. But I want to do it through multiclock assertion without any always block, if possible.

Nope, relation between clkA & clkB is not specified. And out is deliberately kept asynchronous. (Though x[2] & x[1] will change in sync with clkB, and hence out also will change in sync with clkB) — Karan Shah, Oct 14 '15 at 08:47
Sorry, did not see that properly `out` will change in relation to clkB. Thought it was an XOR between clock domains. — Morgan, Oct 14 '15 at 10:10
@Morgan : No Problem, but I need an assertion to verify "out" — Karan Shah, Oct 14 '15 at 14:17

Hida · Accepted Answer · 2015-10-29T15:11:01.880

Disclaimer: I have not tested this.

Have you tried:

#1 @(posedge clkA) (1'b1, t ^= in) |-> 
#2 @(posedge clkB) (1'b1, x[0] = t) |=> 
#3 @(posedge clkB) (out == x[2] ^ x[1], x[1] = x[0]) |=>
#4 @(posedge clkB) (out == x[2] ^ x[1], x[2] = x[1]);

That is, with a overlapping implication in the clock handover. In my experience a non-overlapping implication will cause the assertion to sample not on the next clkB, but skip one clkB and then sample on clkB.

Furthermore I don't quite understand why you are using implications all the way through your assertion. Line #2 is not e prerequisite for line #3, and the same can be said for line #3 and line #4. The way I read this the assertion should start on every clkA, and then a sequence will always follow. In that case the following would be more correct, although the previous code might still work.

@(posedge clkA) 
    (1'b1, t ^= in) |-> 
@(posedge clkB) 
    (1'b1, x[0] = t) ##1 
    (1'b1, x[1] = x[0]) ##1 
    (out == x[2] ^ x[1], x[2] = x[1]);

Lastly, what happens if clkA is much faster than clkB? Several assertions will start in parallel and disagree on the actual value of t on the first posedge of clkB. I must admit that I am hazy on the scoping of values local to a property, but check if this is causing you troubles. A possible fix might be to declare the variable t outside the property scope. Thus t will be updated to the new value on every posedge of clkA and you will have n assertions checking the same thing(which isn't a problem).

Edit: I removed the out == x[2] ^ x[1] check from line #3 because x is local to the property. Thus you cannot check the value made by some other instance of this assertion.

Addition: If the above doesn't work, or if it seems like a waste to start parallel assertions checking the same thing, the following code might work.

Edit2: Put x inside property and changed two final lines in property to update x to correct values.

bit t;
always_ff@(posedge clkA)
     t ^= in;

property p1;
bit[2:0] x;
@(posedge clkB) 
    (1'b1, x[0] = t) |=> 
    (1'b1, x[1] = x[0]) ##0 (1'b1, x[0] = t) ##1 
    (1'b1, x[2] = x[1]) ##0 (1'b1, x[1] = x[0]) ##0 out == x[2] ^ x[1];
endproperty

Bonus tip at the end: The flipflops created should have resets. That is, both x and temp should have resets local to their individual clock domains. The reset can be synchronous or asynchronous as you choose. This must also be added to your property. Also: always use always_ff or always_comb, never use always.

Asynchronous reset:

always_ff @ (posedge clkA or posedge arstClkA)
if(arstClkA)
    temp <= 0;
else
    temp <= temp ^ in;

The problem with use of t is that, it is local to individual instances of the assertion. So if the same assertion is triggered twice, then I believe 2 different variable t will be used for both assertion. And hence everytime, in the assertion t will be 0 ^ in instead of previous t ^ in, which definitely, we do not want. — Karan Shah, Oct 28 '15 at 12:59
If I understand you correctly, this was my point exactly. Because `t` is declared inside the property like this: `property ..; bit t; ... endproperty`it will be local to each instance of the assertion. But, if you declare `t` outside the property like this `bit t; property ..; ... endproperty`. `t` will be updated on _every_ posedge clkA. Thus if clkA is three times as fast as clkB three assertions will be started and each assertion will check exactly the same thing. — Hida, Oct 29 '15 at 09:17
Yes exactly same I tried, but I am getting compile error on assignment of t, when t is declared outside of property. — Karan Shah, Oct 29 '15 at 14:34
See the newest version of the assertion using always_ff to update t. Now there should not be any assignments to values declared outside the property, and `x` should update to the correct value. (The old version would always end up with x[2]^x[1] = 0 because x would equal {t0, t0, t0}. Now it should be {t0, t1, t1} in the final comparison.) — Hida, Oct 29 '15 at 15:16

Multiple Clock Assertion in Systemverilog

1 Answers1