Jump to content

SV assertion comparing multicycle data bus - specific question

Recommended Posts

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?)
Link to comment
Share on other sites

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));

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




Link to comment
Share on other sites

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 




Ajeetha, CVC



Link to comment
Share on other sites

  • 2 weeks later...
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);

   property new_data_0_works;
      logic [1:0] prev_data;
      (valid, prev_data = data) ##1 ~valid[*0:$] ##1 (!new_data && valid) |-> (data === prev_data);
   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.");

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

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

   task clock(input int my_type);
      @(posedge clk);
      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

   always@(posedge clk) begin
      $display($time, "   valid=%1b, new_data=%1b, data=%1x",valid,new_data,data);
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;


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.

Link to comment
Share on other sites

Join the conversation

You can post now and register later. If you have an account, sign in now to post with your account.
Note: Your post will require moderator approval before it will be visible.

Reply to this topic...

×   Pasted as rich text.   Paste as plain text instead

  Only 75 emoji are allowed.

×   Your link has been automatically embedded.   Display as a link instead

×   Your previous content has been restored.   Clear editor

×   You cannot paste images directly. Upload or insert images from URL.

  • Create New...