SV assertion comparing multicycle data bus - specific question

[ljepson74]

Assertion experts,  

 

I know how to do a check of new_data_io (see below) in terms of 'regular' SV code, but will someone comment on how/if I can put this into a nice assertion to put into my interface?

 

All based on posedge clk:

valid_io    - indicates valid data 
data_io     - the data
new_data_io - signifies that data_io has changed since the previous valid_io cycle

 

 

So, when (valid_io && (!new_data_io)), the receiver can just use the most recently valid data.

 

(The fact that there can be cycles of !valid_io, while this assertion is active, is what's throwing me off.  Well, and also the concept of retaining previous state of data_io.  Perhaps this might not be suitable for an assertion and I should just stick with a small process to do the check.)

 

 

thx for any feedback,

Assertion Novice

 

(Why ever did I loan out my book Art of Verification with SystemVerilog Assertions  by Faisal Haque?)

 

[apfitch]

How about:

 

default clocking cb @(posedge Clk); endclocking

property new_data_io_detects_change;
     var logic 7:0] original_data;
     (valid_io, original_data = data_io) ##1 !valid_io[*0:$] ##1 new_data_io |-> (data_io !== original_data));
endproperty

assert new_data_io_detects_change;

Which I hope says "valid_io (capture data_io) followed by 0 or more !valid_io followed by new_data_io implies data_io != captured data_io

 

regards

Alan

[ajeetha]

SVA has $stable() value change system function to do this for you. It returns a boolean indciating its argument was stable across 2 "sampling events". The result can be used as a boolean expression. Now depending on how often data_io changes you may want to fine tune it, but a raw code would be:

 

  always @(posedge clk) begin : b1

    new_valid_io <= valid_io && !($stable (data_io));

  end : b1 
 

 

HTH

 

Ajeetha, CVC

www.cvcblr.com/blog

 

[ljepson74]

Thank you very much Alan and Ajeetha.  Ajeetha, I have not tried $stable yet, but it is on my list to do.

I've played around with my version of Alan's example quite a bit and discovered that I needed to qualify the third stage** of the assertion with a check that valid==1.

Thank you both for your help.

 

**I'm not sure if 'stage' is the proper term.

 

Below is my working code and crude testbench (using irun 12.2-s004).

 

You'll notice that I created two assertions.  One to check that "new_data==1" works and one to check that "new_data==0" works.  If anyone knows a readable way to combine these into a single assertion, please share.

 

module top;
   bit   clk;
   logic valid, new_data;
   logic [1:0] data;

   property new_data_1_works;
      logic [1:0] prev_data;
      (valid, prev_data = data) ##1 ~valid[*0:$] ##1 (new_data && valid)  |-> (data !== prev_data);
   endproperty

   property new_data_0_works;
      logic [1:0] prev_data;
      (valid, prev_data = data) ##1 ~valid[*0:$] ##1 (!new_data && valid) |-> (data === prev_data);
   endproperty
   
   always begin  #5 clk = ~clk;  end

   new_data_yes : assert property (@(posedge clk) new_data_1_works) else begin
      $warning("OUR ASSERTION new_data_1_works FAILED.");
   end

   new_data_no  : assert property (@(posedge clk) new_data_0_works) else begin
      $warning("OUR ASSERTION new_data_0_works FAILED.");
   end

   initial begin
      clk = 1;  valid=0;   new_data=0;
      #14;
      repeat (10) begin  clock(1);  end
      repeat (10) begin  clock(2);  end
      repeat (10) begin  clock(3);  end
      repeat (10) begin  clock(4);  end
      $finish;
   end

   task clock(input int my_type);
      @(posedge clk);
      #2;
      case (my_type)
        1 : begin valid=1'b1;     new_data=1'b1;      data=$urandom;  end
        2 : begin valid=1'b1;     new_data=1'b0;      data=$urandom;  end
        3 : begin valid=1'b1;     new_data=$urandom;  data=$urandom;  end
        4 : begin valid=$urandom; new_data=$urandom;  data=$urandom;  end
        default : begin valid=1'bX; end
      endcase
   endtask

   always@(posedge clk) begin
      $display($time, "   valid=%1b, new_data=%1b, data=%1x",valid,new_data,data);
   end
endmodule : top 

 

//Notes to self
/*Put this into the initial block and use this in place of the top assertion.  Note the missing valid in 3rd stage.
      (valid, prev_data = data) ##1 ~valid[*0:$] ##1 (new_data)  |-> (data !== prev_data);

      //Here I showed to myself that I must must qualify the 3rd stage of the above assertions
      // with valid being true. (ex: new_data && valid)
      //This is done by trying to make new_data_yes fail on a non-valid cycle here.
      //
      // Below, two cycles of 'good' data is generated.
      // Then valid is dropped to 0 (entering the 2nd stage of the assertion - I don't know correct terminology for this).
      // Then without raising valid to 1, we can move to the 3rd stage by setting new_data=1.  (which was my problem)
      // I suppose I had focused on the "~valid[*0:$]" being what controlled when we moved to the 3rd stage of the assertion, but 
      // realize now that is not correct.
      // The 2nd stage can stay true (i.e. valid=0) for as long as it will, but each clock we are just looking for what is after
      // the "##1" to move on to the next stage.  In this case, new_data==1.

      @(posedge clk); #2; valid=1'b1;     new_data=1'b1;      data=2'b10;
      @(posedge clk); #2; valid=1'b1;     new_data=1'b1;      data=2'b01;
      @(posedge clk); #2; valid=1'b0;     new_data=1'b0;
      @(posedge clk); #2; valid=1'b0;     new_data=1'b0;
      @(posedge clk); #2; valid=1'b0;     new_data=1'b1;    //error will fire now b/c new_data==1.
      @(posedge clk); #2; valid=1'b0;     new_data=1'b1;
      $finish;
*/

 

Thanks again.

 

 

 

Thinking more about my question of combining the assertions, I am wondering why the implication operator would be used at all, and why I couldn't just do a check like

 

(   valid &&   (  (new_data && (data!==prev_data)) || (!new_data && (data===prev_data))  )   )

 

I'll experiment with this later.   

Comments very welcome.