How to use recursive properties in Systemverilog

Question

The module to be verified is as follows... The module has an input in1 and an output out1, on alternating clock cycles, out1 is the buffered and inverted value of in1.

I tried coding the checker module using a recursive property.

module check (input in1, out1, clk);

    property p1(bit state);
        bit nxt;
        @(posedge clk) 
        (1 ,nxt=!state) |-> (out1 == (nxt) ? !in1 : in1) and 
                             nexttime p1(nxt);
    endproperty

    initial assert property(p1(0)) else $fatal(3, "Failed!");

endmodule

However, running the code at edaplayground throws this error...

RROR VCP2000 "Syntax error. Unexpected token: nexttime[_NEXTTIME]. The 'nexttime' is a SystemVerilog keyword and cannot be used as an identifier.

I know that this assertion can be done without recursion but I would like to use recursion to write it.

Answer 1

The error says that you have used nexttime which is a systemverilog property keyword in a wrong manner. This operator checks that "if the clock ticks once more, then a shall be true at the next clock tick" in the following code

property p1;
  nexttime a;
endproperty

By default, the concurrent assertions shall be checked on every clock pulse, so there is no need of recursion here. Roughly, you can do something like this:

module check (input in1, out1, clk);
bit o_nxt;

function bit update(input bit nxt);
o_nxt = nxt;
return 1;
endfunction

    property p1(bit state);
        bit nxt;
        @(posedge clk) 
        (1 ,nxt=!state) |-> (out1 == (nxt) ? !in1 : in1) and 
                             update(nxt);
    endproperty

    initial assert property(p1(o_nxt)) else $fatal(3, "Failed!");

endmodule