Jump to content

assertion to check for an array of channels

Recommended Posts

Consider the following code and the assertion to check for unknown data.


If the code will change so that there will now be an array of valids and datas, what is the best way to change the assertion, so that for each valid, the corresponding data is checked.?

Can I do it one line?   (I had been considering using a generate statement around it.)

module top;

   bit   clk;
   logic write_valid;
   logic write_data;

   always clk = #5 !clk;

   initial begin

   as_showme : assert property (@(posedge clk) disable iff (!write_valid) (!$isunknown(write_data)) ) else begin
      $display("*** ERROR. write_data was unknown. ***");

Link to comment
Share on other sites

I'd start off with comments on your current assertion. You shouldn't use write_valid inside the disable iff block of the assertion. That's because it won't do what you probably think it does (at least not in SV 2012). The disable iff is for asynchronous resets, but I'm guessing that write_valid is a synchronous signal.


What I think you want is:

write_valid |-> !$isunknown(write_data)

If for some reason you don't like the fact that this property accepts vacuous successes (i.e. it's true when write_valid is 0), then you can use disable iff to disable it in those case, but you need to make sure to use $sampled(...):

disable iff (!$sampled(write_valid))

This way you won't get any race conditions due to changing write_valid. You can read up more on the topic in section 16.2 Declaring properties of the SV2012 LRM, page 388.

Link to comment
Share on other sites

As Tudor said we need to we shouldn't use write_valid in disable iff  if it is synchronous value. write_valid and write_data are array then I would use following code:

  property p_write_valid_no_unknown_write_data(a_write_valid,a_write_data);
    @(posedge clk) disable iff (!as_rst_n)
          (a_write_valid) |->!$isunknown(a_write_data);

  genvar i;
    for(i= 0; i<=ARRAY_SIZE_i=i+1)
     begin: write_valid_write_data
       ast_write_valid_write_data: assert property (p_write_valid_no_unknown_write_data(write_valid[i],write_data[i]) 
                                     $error($psprintf("ASSERTION_ERROR:write_valid[%0d]: write_data:%0h",i, write_data[i));



Link to comment
Share on other sites


 Thank you very much.


 I had considered these following variations (and will now make doubly sure they're clear in my mind):

  disable iff (write_valid) !$isunknown(write_data) //use disable iff for asynchronous disabling

  write_valid |-> !$isunknown(write_data) //Recommended

  !(write_valid && $isunknown(write_data)) //***See below

 I had not thought about synchronicity with regards to disable iff, so thanks a lot for enlightening me, Tudor.  (***And in another post we discussed implication versus logical AND.  http://forums.accellera.org/topic/5407-overlapped-implication-vs-logical-and-vs/ )


 , ... but the focus of the topic, which I may not have presented clearly enough was what Tinku showed.   I was hoping there was some way to avoid using a generate, but that solution seems very clear.


 Thank you for shedding light on parts of the example I hadn't even thought much about yet.

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...