Hi,
I am trying to create a recursive property and I am getting this error:
Disable iff can not be used inside recursive properties.
The associated code is this one:
timeunit 1ns;
timeprecision 1ps;
module test();
`define WD [64-1:0]
`define NB 2
reg clk_i;
reg rsn_i;
reg [2:0] len_i;
reg `WD data_i;
reg write_en_i;
wire [127:0] out;
wire ready;
assign len_i = 3'b111;
assign data_i = 'b1;
assign out = 'b1;
assign write_en_i = 1'b1;
assign ready = 1'b1;
always begin
clk_i =1'b1;
#10;
clk_i=1'b0;
#10;
end
initial begin
rsn_i=1'b0;
#30;
rsn_i=1'b1;
end
property p_correct_chunk_value (
local input logic [`NB-1:0]`WD piece,
local input int unsigned length
);
logic [`NB-1:0]`WD piece_ = piece;
logic length_ = length;
if (length > 0)
(
(write_en_i, piece_[length_-1] = data_i `WD)
|=>
p_correct_chunk_value(piece_, length_-1)
)
else
(
##[1:$] ready && piece == out
);
endproperty
property p_correct_recur (local input int unsigned length);
logic length_ = length;
if (length%`NB == 0)
(
p_correct_chunk_value('b0, `NB)
and
p_correct_recur(length_-`NB)
)
else(
if (length == 0)
(
1'b1 // Exit condition
)
else
(
p_correct_chunk_value('b0, length)
and
p_correct_recur(0)
)
);
endproperty
property p_correct (clk, rsn);
@(posedge clk)
disable iff (!rsn_i)
p_correct_recur(len_i);
endproperty
assertion : assert property (p_correct(clk_i, rsn_i));
endmodule
When declaring the assertion I DO NOT USE
disable iff
Why this error? The compiler is not pretty intuitive.
Thanks in advance.