ljepson74 Posted January 26, 2016 Report Share Posted January 26, 2016 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 clk=0; write_valid=0; #7; write_valid=1; #100; $finish; end as_showme : assert property (@(posedge clk) disable iff (!write_valid) (!$isunknown(write_data)) ) else begin $display("*** ERROR. write_data was unknown. ***"); end endmodule Quote Link to comment Share on other sites More sharing options...
tudor.timi Posted January 26, 2016 Report Share Posted January 26, 2016 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)) !$isunknown(write_data) 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. ljepson74 1 Quote Link to comment Share on other sites More sharing options...
tudor.timi Posted January 26, 2016 Report Share Posted January 26, 2016 Next up, what do you mean with write_valid and write_data are in arrays. Do you have more signal pairs that you need to check? Quote Link to comment Share on other sites More sharing options...
tinku Posted January 26, 2016 Report Share Posted January 26, 2016 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); endproperty genvar i; generate 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]) else $error($psprintf("ASSERTION_ERROR:write_valid[%0d]: write_data:%0h",i, write_data[i)); end endgenerate Quote Link to comment Share on other sites More sharing options...
ljepson74 Posted January 26, 2016 Author Report Share Posted January 26, 2016 Tudor/Tinku, Thank you very much. I had considered these following variations (and will now make doubly sure they're clear in my mind): //i) disable iff (write_valid) !$isunknown(write_data) //use disable iff for asynchronous disabling //ii) write_valid |-> !$isunknown(write_data) //Recommended //iii) !(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. Quote Link to comment Share on other sites More sharing options...
Recommended Posts
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.