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.
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.
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