In reply to a72:
Is this what you are looking for?
bit lk;
function void set_lk(bit x);
lk=x;
endfunction
assert property(@ (posedge clk)
(st==S1 && !lk, set_lk(1)) |->
not((st==S1 ##1 st==S2) [*32]))
set_lk(0); else set_lk(0));
Ben systemverilog.us