Legal ways to specify the leading clock in SVA

SystemVerilog
,
12

In reply to ben@SystemVerilog.us:

Hi Ben,
If it’s not too much to ask, I would like to hear your thoughts on (3) only


 always@(posedge clk)  begin
     if ( bstate )  begin
       @(negedge regcheck);
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end

Shouldn’t it be equivalent to


   property  pr1;
     @(posedge clk) bstate ##1 @(negedge regcheck) |=> @(posedge clk) a ##2 b;
   endproperty
   assert  property( pr1 );