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.

Answer 1

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;