Multiply clock sequence

SystemVerilog
, , ,
1

Hey guys! I’m new in SVA and also in Formal Verification.
I want to write an assertion like the description bellow:

GCK1 need 1cycle CLOCK1 to update value of A
GCK2 need 1cycle CLOCK2 to update value of !A
and, OUT= GCK1 OR GCK2
So, I have one test item is: when A HIGH, OUT also HIGH at second posedge of slower clock

this is my assertion


sequence seq(clock,_out,_a);
   @(posedge clock) ##1 _out==_a;
endsequence
assert_out: assert property(
   (a==1) |-> seq(clock1,out,1) OR seq(clock2,out,1);
);

and … it failed.
Do you have any ideal?, thank so much!

2

In reply to kiennt_0543:

(a==1) |-> seq(clock1,out,1) OR seq(clock2,out,1); // WILL NOT compile!

The issue here is that every assertion needs a leading clocking event.
A leading clocking event of an assertion directive is the clocking event that starts the property of the assertion directive. An assertion may have more than one clocking event, such as those in multiclocked properties; however, there is only one leading clocking event in any assertion statement. Here is your fix. You need to assess the need for 2 separate assertion directives, each with a different leading clocking event.


sequence seq(clock,_out,_a);
   @(posedge clock) ##1 _out==_a;
endsequence
assert_out1: assert property(
   @(posedge clock1(a==1) |-> seq(clock1,out,1) OR seq(clock2,out,1);
);
assert_out2: assert property(
   @(posedge clock2(a==1) |-> seq(clock1,out,1) OR seq(clock2,out,1);
);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy