Assertion and stable value from the beginning

SystemVerilog
7

In reply to Srini @ CVCblr.com:

Love when co-authors disagree! With this code:

module test_1time2 (
		input clk, started, enb, rst_n,
		output x_out); 
	bit first_rise_in_enb_detected;
 
  always_ff @(posedge clk iff !first_rise_in_enb_detected) begin
    if (!enb)
       first_rise_in_enb_detected = 0;
    else
       first_rise_in_enb_detected = 1;
  end
 
  ap_xout: assert property (@(posedge clk) !first_rise_in_enb_detected |-> x_out == 0);
endmodule

the formal verification tool will toggle enb within the evaluation of the assertions. Thus, the variable first_rise_in_enb will toggle multiple times within the evaluations, and ap_xout assertion will be evaluated multiple times. You need assume statements to constraint the behavior of enb.
This is what I did with

am_1time: assume property(@(posedge clk) $rose(enb) |-> started==1); 
am_started: assume property(@(posedge clk) $rose(started) |-> started==1);

:)
Ben SystemVerilog.us