In reply to MSB:
That extra @(posedge clk) is NOT needed on the RHS of non overlapping implication operator. It is not needed because the initial clocking event (i.e., the one in the @(posedge clk) disable iff (!freqed_valid)) flows through to the consequent.
And NO, that extra @(posedge clk) does not adds one more clock cycle to the calculation. That extra clocking event is typically used in multiclocking. Fro example:
ap0: assert property(@(posedge clk1) $rose(a) |-> @(posedge clk2) b);
If you use the same clocking, it is considered a multiclocking where the 2nd clocking event is in sync with the first.
BTW, I had it because I copied your assertion and was concentrated on your initial problem of block error message and not the assertion itself. Actually, you do not needed and it is confusing if you do add it. Remeber, the clock flows from the antecedent to the consequent.
SVA has specific rules on clock flow and sequences. The LRM explains them, and I demonstrate them in my SVA BOOK (4.3 Clocked Sequences, Properties, And Multiclocking).
Ben SystemVerilog.us