For the most part, these relations are simple. Like in CCSL, there is a operator ‘Subclock’ that relates as ‘A isSubClockOf B’ means when there is an event on A, B must also be present but not the other way around. And we both know that this is the same as |-> of SystemVerilog Assertions.
But some other operators are not so much compatible like ‘Asfrom’ mentioned on page 13 of this report(4). For this Asfrom relation, the output signal O shouldn’t consider first k events and after that is coincident with the A. Apparently this relation should work for k = 5.
$rose(rst) ##1 ((a[=5]) intersect (!o[*])) |=> ((a ~^ o)[*0:1000]); // interval 0:1000 is used instead of 0:$
where I use the XNOR operator to check the resemblance of signals after the trigger k. But somehow it works fine for the part before the implication but not afterwards. I feel I lack some concepts about the working of SVAs here.