Assertion protocol checker

In reply to ben@SystemVerilog.us:

ok, so upon some reflection, I get how……:


function  void set_started(bit a); 
        started = a; 
    endfunction : set_started   
    // 1 - every start is followed by an end or a stop (start to start back to back cannot occur)
    ap_start_stopr_or_done: assert property( 
      (start, set_started(1)) |=> stop[->1] or done[->1]) 
      set_started(0); else set_started(0);


… is working. well… to my limited understanding I see this as the mechanism to call the function controlling the flag status, based on the sequencing of the start/stop and done.
This assertion never fails (?)

to my eyes, and very much in the style of “many different ways of skinning a cat”, would the following have not achieved the same:


always @(posedge clk or negedge !rst_n)
        if (!rst_n) started <= '0;
        else begin
            if (start) started <= '1;
            else if (done || stop) started <= '0;
        end

a little more supporting logic? but to my eyes (I suppose as a less hardcore ABV experienced engineer) easier to follow?

am I right? do they achieve the same thing?