Difference between two assertions

SystemVerilog
,
1

The specification is written below
Specification:

  1. If Frame_ is high then Frame_ must be low the very next cycle (1 clock pulse) and remain low until the next strictly subsequent cycle in which IRDY_ is high.
  2. IRDY_ can be high only if Frame_ was high and that IRDY_ was not high in any of the intervening cycles.

The solution for above question is
Solution:

Assertion author solution

  1. Frame_to_IRDY: assert property (Frame_ |=>!Frame_ throughout IRDY_ [->1]);
  2. IRDY_to_Frame_: assert property (IRDY_ |=>!IRDY_ throughout Frame_ [->1] );

My solution

  1. Frame |=> !frame through !IRDY[*0:$] ##1 $rose(IRDY);

Is my solution is right? if it is wrong may, I know why it is wrong?

2

A few questions
(1) Is through a legal keyword ?
(2) What is the equivalent expression for IRDY_ [->1]) ?

3

See my paper

Addresses the usage of these four relationship operators: throughout, until, intersect, implies
Your solution is the same as

  1. Frame_to_IRDY: assert property (Frame_ |=>!Frame_ throughout IRDY_ [->1]);
    en Cohen
    Ben@systemverilog.us
    Link to the list of papers and books that I wrote, many are now donated.
    https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf