Counting number of events on clock a, while clock o is forbidden

SystemVerilog
, ,
3

In reply to ben@SystemVerilog.us:

Thanks Ben for the reply, Its great feeling to talk to the author whose book I am following these days. Sorry that my question wasn’t that clear. I am actually using SVAs in a research context, so the requirements are quite strange. Also I am not much experienced with SVAs. But I am quite hopeful that it will be a case-study to help other researchers having same issues.

My design consists of two clocks A and O and a variable K (which is 5 for now). The clocks A,O are logical meaning the clock events can come at random intervals, but synchronously on the system clock (from 1 cycle to many cycles). By clock event we don’t necessarily mean the rising edge event (on A), it can be that the value of A is sampled 1 on the rising edge of clk. The expression
O = A asfrom K

, where k is a natural number, defines a clock that is a tight sub-clock of A starting after index K. For example, the event O occurring on the 3rd or 9th clock of A will generate a violation. or event O occurring while the event A is not there will also cause violation. Here is the picture showing one possible execution of events:
http://postimg.org/image/gqkom70y7/

I have got one solution to this problem but it is based on the use of external variable cnt (count):


module AsFrom();
  reg clk,a,o;

  initial 
  begin
    clk=0;a=0;o=0;
    #200
    a=1; #100 a=0;          // a
    #100
    a=1; #100 a=0;          // a 
    //#100
    //o=1; #100 o=0;        // o, will cause violation
    #200
    a=1; #100 a=0;          // a 
    #200
    a=1; #100 a=0;          // a
    #100
    a=1; #100 a=0;          // a 
    //#100
    //a=1; #100 a=0;        // a, will cause violation
    #200
    a=1;o=1; #100 a=0;o=0;  // a,o 
    #200
    a=1;o=1; #100 a=0;o=0;  // a,o 
    #300
    a=1;o=1; #100 a=0;o=0;  // a,o 
    #100
    a=1;o=1; #100 a=0;o=0;  // a,o  
    #200
    a=1; #100 a=0;          // a, will cause violation
    #200
    o=1; #100 o=0;          // o, will cause violation
  end

  always #50 clk = ~clk; 
  
  int cnt=0; 
  const int k=5;   
  always @(posedge clk) begin
      if (a && (cnt < k)) cnt++;
  end
  
  // As From
  property AsFrom;
    @(posedge clk)    
    o |-> (a && cnt==k);
  endproperty
  assert property (AsFrom);
  
endmodule

I want to get the solution based on assertions only. I feel the non-consecutive repetition operator [=5] would be used something like,
rose(rst) ##1 A[=5] |=> (A && O)[=1:];

But it doesn’t forbid the clock O. There is a solution in your book using local variables that looks interesting, i quote:


property pWriteNstart;
   int v_start, target_size;
   ($rose(cmd==WRITE), v_start=0, target_size=size)
   |=>first_match(
   (##[0:$] (gx_start, v_start=v_start+1))[*1:$] ##0 v_start==target_size
   ) |-> data_last;
endproperty : pWriteNstart

But i couldn’t relate it to my problem. Moreover, one further question can we have a solution for if we have no reset signal rst? can we still count the clock events on A? Will each event not start a new thread for the antecedent (for which first_match may help)?

One auxiliary question, my copy of questasim 10.0c doesn’t support ‘until/until_with’ so i couldn’t try this command. Is it possible to do ‘A until B’ on logical clocks any other way?

Thanks again for your reply and time, it may help many in the future.

Aamir