Search the Community

I recently encountered SVA code which results in different results on different simulators. I've shrunk it to a simple example here. I believe this code should cause an error, but it does not on all tools. Can someone comment on how the 2017 LRM should be interpreted (and perhaps on the code). (I sense someone will comment on the driving signals in the code.) module top; bit clk; logic sig1; logic disable_assert; always begin #5 clk=0; #5 clk=1; end initial begin disable_assert=1'b1; sig1 =1'b0; $display("Hello World"); $monitor($time," **** sig1:%0b disable_assert:%0b",sig1, disable_assert); repeat (3) @(posedge clk); @(posedge clk); sig1=0; disable_assert=1; @(posedge clk); sig1=1; disable_assert=1; //2a. assertion would fail, but it is disabled @(posedge clk); sig1=0; disable_assert=0; //2b. now assertion is enabled and should fail** @(posedge clk); sig1=0; disable_assert=1; #20; $finish(); end property as_disable_testing; @(posedge clk) disable iff (disable_assert) !sig1; endproperty assert property (as_disable_testing); endmodule : top Question: Should there be a timing error at comment 2b, or not? Code is here to play around with: https://www.edaplayground.com/x/njR Picture: https://docs.google.com/drawings/d/1qQB4dB5w8_1jx73xta46RbmLzkparaNcxHNdLgi8YNY/edit?usp=sharing These are my thoughts: // It seems this small code snippet should cause an error, but tool results differ. // // // NOTE: Yes, I realize that I am using tools from BEFORE 2017, but comparing results to the 2017 LRM. // What is the correct LRM interpretation? What comments do gurus have about this code? // // //1) Run the code with Aldec Riviera Pro 2015.06, Synopsys VCS 2014.10, and with Cadence Incisive 15.20. // RIVIERA PRO and IRUN show assertion failures. // VCS does not show assertion failure. // //2a) This is time when sig1=1 assertion 'would' fail, but it is disabled (disable_assert==1) //2b) **On next clock cycle the assertion set to be enabled (i.e. disable_assert==0). // The SystemVerilog 2017 LRM (1800.1-2017.pdf) describes the behaviour. // At the start of the 2b time slot (see page 64 of SystemVerilog LRM 1800.1-2017), // PREPONED REGION: the values of the assertion are sampled (sig1==1) // ACTIVE/INACTIVE/NBA regions: the values are updated (sig1,disable_assert) // (so you can use either blocking "=" // or you can use non-blocking "<=" // and you will get the same result) // So for this time slot: sig1==0, disable_assert=0 // OBSERVED REGION: this is where the assertion is evaluated, using values sampled from // the preponed region (so sig1==1). // However, the value of disable_assert is not from the // preponed region, but simply whatever the value is, // as assigned in the active/inactive/nba region. // // // Section 16.6 of the SystemVerilog LRM (1800.1-2017 states: "The expressions in a disable condition are evaluated using the current values of variables (not sampled) ..." I believe this means from whatever is set in the Active/NBA region of current time slot. // // Section 16.12 of the same document states: "If the disable condition is true at anytime between the start of the attempt in the Observed region, inclusive, and the end of the evaluation attempt, inclusive, then the overall //evaluation of the property results in disabled." // // My conclusion: The sig1 value from 2a will be used in 2b when disable_assert=0; ***Assertion should fail.*** // // Picture: https://docs.google.com/drawings/d/1qQB4dB5w8_1jx73xta46RbmLzkparaNcxHNdLgi8YNY/edit?usp=sharing

I happened across the following code. @(m_vif.smp_cb iff (m_vif.smp_cb.xyz_enable) ); To get to the crux of my question, let's consider it to be the below code. I don't think I've dropped anything relevant with this change (but I post both, b/c I have dropped important info with my edits in the past). @(posedge clk iff (xyz_enable) ); Q) How should the above line behave? How would you read that line aloud? 1) "Wait for a posedge of clk, if and only if xyz_enable is true." //That's how I read it, but that is incorrect. 2) "Wait for posedges of clk until xyz_enable is true." //This is correct. My thought was that when xyz_enable==0, it would just 'fall through' and there would be no wait for a posedge of clk. i.e. if(xyz_enable) @(posedge clk); Can someone help me read that line as a descriptive sentence? Here is some test code: module top; logic clk; int count=0; initial clk=0; always #1 clk = ~clk; initial begin $display($time," ************* START"); repeat (10) @(posedge clk); fork begin repeat(33) begin $display($time," Tine1: waiting for posedge clk. count=%0d",count); @(posedge clk); count++; end end begin $display($time," Tine2: waiting for count=10"); @(posedge clk iff (count==10)); $display($time," Tine2: waited for count=10. count=%0d",count); end join_any $display($time," ************* END"); $finish; end endmodule Results: 0 ************* START 19 Tine1: waiting for posedge clk. count=0 19 Tine2: waiting for count=10 21 Tine1: waiting for posedge clk. count=1 23 Tine1: waiting for posedge clk. count=2 25 Tine1: waiting for posedge clk. count=3 27 Tine1: waiting for posedge clk. count=4 29 Tine1: waiting for posedge clk. count=5 31 Tine1: waiting for posedge clk. count=6 33 Tine1: waiting for posedge clk. count=7 35 Tine1: waiting for posedge clk. count=8 37 Tine1: waiting for posedge clk. count=9 39 Tine1: waiting for posedge clk. count=10 39 Tine2: waited for count=10. count=10 39 ************* END Thanks, for any feedback.