I have written a assertion as below to verify command=2 doesnot happen more than 4 times in 60 clock cycles but seeing a compilation issue for sequence sequence_60_cycles;
module tb();
bit clk;
bit [1:0] cmd;
initial begin
clk = 0;
forever #5 clk = ~clk;
end
sequence cmd_seq;
(cmd[1:0] == 2'b10) [=4:$];
endsequence
sequence seq_60_cycles;
##60;
endsequence
property command_2_in_60_cycles;
int tmp;
@(posedge clk)
// int tmp;
(cmd[1:0] ==2'b10) |-> not( cmd_seq) within seq_60_cycles;
endproperty
A1 : assert property(command_2_in_60_cycles);
initial begin
$dumpfile("dump.vcd");
$dumpvars;
#600 $finish;
end
initial begin
repeat(20) begin
@(posedge clk);
cmd = $random;
end
repeat(200) begin
@(posedge clk);
cmd = 2'b11;
end
end
endmodule
Error-[SE] Syntax error
Following verilog source has syntax error :
“testbench.sv”, 19: token is ‘;’
##60;
Your assertion is probematic because of the within and [=4] (more than 1 )
See the last example in my paper on Degeneracy
Paper: Understanding SVA Degeneracy
A MUST READ PAPER FOR SVA USERS!
sequence cmd_seq;
(cmd[1:0] == 2'b10) [=4:$];
endsequence
sequence seq_60_cycles;
##60;
endsequence
property command_2_in_60_cycles;
int tmp;
@(posedge clk)
// int tmp;
(cmd[1:0] ==2'b10) |-> not( cmd_seq) within seq_60_cycles; // probematic because of the within and [=4] (more than 1 )
endproperty
A1 : assert property(command_2_in_60_cycles); // BAD,
A2_better: assert property(@(posedge clk) (cmd[1:0] ==2'b10) |=>
not (cmd_seq==2'b10[=5:60] intersect 1 [*60]);
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
This is better
A2_better3: assert property(@(posedge clk)
(cmd[1:0] ==2'b10) |=>
(cmd_seq==2'b10[=0:4] intersect 1 [*60]);
I never liked the “not” operator.
Ben,
I observe following 2 issues with your code
- Goto and nonconsecutive repetition operators are not valid for sequences.
i.e cmd_seq[=0:4] would be illegal
- If I re-write consequent to
(cmd[1:0] == 2'b10)[=0:4] intersect 1 [*60]);
Due to [=0] the consequent admits empty match and violates the quote from
LRM 16.12.22 Nondegeneracy
Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
One possible way to avoid (2)
assert property(@(posedge clk) ( (cmd[1:0] == 2'b10)[=1:4] or (cmd[1:0] != 2'b10)[*60] ) intersect 1 [*60]);
From my degeneracy paper
b[=0] // is equivalent to:
##0 !b[*0]) or (##0 !b[*1:$])
Thus, you are correct in that due to [=0] the consequent admits empty match and violates the quote from
2.LRM 16.12.22 Nondegeneracy*
Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
I like your solution
assert property(@(posedge clk) ( (cmd[1:0] == 2'b10)[=1:4] or (cmd[1:0] != 2'b10)[*60] ) intersect 1 [*60]);
I sent this to members of the SV and SVA committee to address this degenracy issue for the next 1800 revision.
Issue:
When faced with degenerate sequences, 1800’2023 is unclear on what a simulator should do, particularly in situations resulting from parameter substitution that creates a degenerate sequence. In that situation, it would be undesirable to have to rewrite the code to get to a successful compilation. Existing tools differ in their interpretation of degenerate sequences - some report it as a degenerate situation, some issue a warning, and some proceed with the simulation.
document identifies the sections in the LRM that define degeneracy and highlights cases that pose challenges for users and tool vendors. Additionally, it proposes solutions for the next revision of the LRM.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
1 Like
Below code worked.
Thanks hdlcohen .
sequence cmd_seq;
(cmd[1:0] == 2'b10) [=5:60];
endsequence
sequence seq_60_cycles;
bit [6:0] counter_60=0;
(1, counter_60 = counter_60+1'b1, $display("The counter value = %0d", counter_60)) ##60 ##0 (counter_60 == 60,$display("End Counter value = %0d", counter_60));
endsequence
property command_2_in_60_cycles;
int tmp;
@(posedge clk)
// int tmp;
(cmd[1:0] ==2’b10) |-> not ((cmd_seq) within seq_60_cycles);
endproperty
COMMAND_4_TIME_IN_60_CYCLES: assert property(command_2_in_60_cycles) else $error(“%0t Assertion got failed”, $time);
COnsider what the assertion should do, instead of what it should not do.
assert property(@(posedge clk) ( (cmd[1:0] == 2’b10)[=1:4] or (cmd[1:0] != 2’b10)[*60] ) intersect 1 [*60]);
Ben
ALso, use the intersect, not the within.
See my paper on the within and the [=2]
