ljepson74 Posted August 14, 2013 Report Share Posted August 14, 2013 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?) Quote Link to comment Share on other sites More sharing options...
apfitch Posted August 15, 2013 Report Share Posted August 15, 2013 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 Quote Link to comment Share on other sites More sharing options...
ajeetha Posted August 18, 2013 Report Share Posted August 18, 2013 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 Quote Link to comment Share on other sites More sharing options...
ljepson74 Posted August 30, 2013 Author Report Share Posted August 30, 2013 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. 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.