Difference between two assertions

The specification is written below

  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

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?

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

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
    Link to the list of papers and books that I wrote, many are now donated.