Search the Community

The below assertions check that gnt is not high for consecutive clk cycles. Q1: v1 vs. v2: Are there benefits or relevant differences between these styles. Q2: v2 vs. v3: Does the placement of delay matter? Besides for end of simulation termination. The questions are mainly about whether some style is better for the simulator, or there is some non-obvious situation I should consider. module top; bit clk, gnt; bit [19:0] gnt_a; initial begin gnt_a = 20'b0011001010_0000001101; #200 $finish; end assign gnt = gnt_a[19]; always clk = #5 ~clk; always@(posedge clk) begin gnt_a = gnt_a<<1; $display($time," gnt: %1b",gnt); end as_v1 : assert property ( @(posedge clk) not strong(gnt[*2]) ); as_v2 : assert property ( @(posedge clk) gnt |-> ##1 !gnt ); as_v3 : assert property ( @(posedge clk) gnt ##1 1'b1 |-> !gnt ); endmodule Code is also available here: https://edaplayground.com/x/4GXn

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

Are are any standard or recommended ways of verifying the functionality of the round-robin arbiter and more specifically checking the fairness? I'm looking for something that is scalable with the number of requestors. Functionality of the arbiter is as follows: - Say there are 3 requestors, req1, req2 and req3. The pointer points to req1 initially. Consider different cases for illustration. - If all 3 requests are asserted, req1 goes through and the pointer is updated to req2. - If req2 and req3 is asserted, then req2 will go through and pointer is updated to req3. - If just req3 is asserted, then req3 will go through and pointer is updated to req1(cyclic). The pointer is always updated to the next requestor that got previously granted - if req1 granted, pointer is updated to req2 - if req2 got granted, pointer is updated to req3, - if req3 is granted, pointer is updated to req1 The pointer points to the requestor that has higher priority for the next round of requests, in order to ensure fairness in the way grants are allotted.

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

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