Verifying a sequence detector not working as expected

[ShashankVM]

Hi Developers,

I'm trying to verify this 1011 sequence detector. Problem is the delay is not as expected, when I set a bigger delay such as 6 cycles and add reset before the sequence it gets proven, but that's incorrect. It's not getting proven for the 2 cycles delay without adding reset before the sequence.

Command used:
ebmc seq_detector_overlapping_ebmc.sv --top seq_detector_overlapping --bound 500 --reset reset==1 --vcd ebmc_counter.vcd

Code:

module seq_detector_overlapping(
   input seq_in, clk, reset,
   output logic detect_out
);

   //one-hot encoding of FSM
   enum logic [4:0] {S0 = 5'b00001, S1 = 5'b00010, S2 = 5'b00100, S3 = 5'b01000, S4 = 5'b10000}  state, next;


   //state registers
   always_ff @(posedge clk or posedge reset)
     if (reset) state <= S0;
     else       state <= next;

   // Next state assignment logic
   always_comb begin
     next = state;
      unique case (state)
       S0 : if (seq_in) next = S1; else next = S0;
       S1 : if (seq_in) next = S1; else next = S2;
       S2 : if (seq_in) next = S3; else next = S0;
       S3 : if (seq_in) next = S4; else next = S2;
       S4 : next = S0;
     endcase
   end

   // Registered output logic
   always_ff @(posedge clk, posedge reset)
     if (reset) detect_out <= 1'b0;
     else       detect_out <= (state == S4);

ASSUME_VALID_STATE: assume property ($onehot(state) and (reset |-> (state == S0)));

ASSERT_CHK_SEQ_DETECT: assert property (@(posedge clk) reset ##1 seq_in ##1 !seq_in ##1 seq_in ##1 seq_in  |-> ##6 detect_out);

ASSERT_BI: assert property ( @(posedge clk)  detect_out |-> (($past(seq_in, 2) == 1) && ($past(seq_in, 3) == 1) && ($past(seq_in, 4) == 0) && ($past(seq_in, 5) == 1)) );

endmodule

[ShashankVM]

This is the property I want to prove
seq_in ##1 !seq_in ##1 seq_in[*2] |=> ##1 detect_out;

[kroening]

I'm trying to verify this 1011 sequence detector. Problem is the delay is not as expected, when I set a bigger delay such as 6 cycles and add reset before the sequence it gets proven, but that's incorrect. It's not getting proven for the 2 cycles delay without adding reset before the sequence.

Just to double-check: with the given model you expect a counterexample?

[kroening]

There is a bug where the sequence implication operator does not pick up the end of the chain sequence on the left hand side. Will fix!

[ShashankVM]

Thanks Dr. Daniel for the fix.
This property is proven now,
ASSERT_CHK_SEQ_DETECT: assert property (@(posedge clk) reset ##1 seq_in ##1 !seq_in ##1 seq_in ##1 seq_in |-> ##2 detect_out);
but this doesn't get proven
ASSERT_CHK_SEQ_DETECT: assert property (@(posedge clk) seq_in ##1 !seq_in ##1 seq_in ##1 seq_in |-> ##2 detect_out);

Can you please suggest? I think we need reset simulation to load the initial state of the flops.

[kroening]

but this doesn't get proven ASSERT_CHK_SEQ_DETECT: assert property (@(posedge clk) seq_in ##1 !seq_in ##1 seq_in ##1 seq_in |-> ##2 detect_out);

Can you please suggest? I think we need reset simulation to load the initial state of the flops.

The tool's response would seem to be correct. If you look at the counterexample, you'll see that the 1011 sequence starts with the reset, and is hence missed.

However, it's not enough to deal with reset -- the next failure is that the model doesn't deal with two overlapping instances of 1011, e.g., 1011011.

[kroening]

BTW, the easy way to build this is a shift register!

[ShashankVM]

Yes I do agree that I have posted a non-overlapping detector here. Both reset simulation and disable iff reset are important features. I'd like to work on this, could you suggest how to get started? I can code in C++.

[kroening]

disable iff got added with #617.

A way to say that you don't want your assertion to say anything about the initial state is to add ##1 (like in the example in #619), or write always [1:$].

[ShashankVM]

Thank you so much, Dr. Daniel. I've written a LinkedIn article on my formal verification project of overlapping and non-overlapping sequence detectors using the updated version of the HW-CBMC tool. You are welcome to give it a read.
Post: https://www.linkedin.com/posts/shashank-v-m_after-dr-daniel-kroening-added-the-code-activity-7226636234930933761-YcSn?utm_source=share&utm_medium=member_desktop
Article: https://www.linkedin.com/pulse/formal-verification-overlapping-non-overlapping-1011-sequence-v-m-mdlwc/?trackingId=ZyeCiH35S16Qbb%2FOVzpgxw%3D%3D