Unexpected gate in partition that causes FAIL checking result

[Manchdog]

I have checked the equivalence between two Verilog descriptions in1.v and in2.v.

The checking result is "FAIL", but the generated counterexample contains inner gate and_32 (in gate design) that is not connected with primary output out_11, while there is and_33 gate that is an input for out_11 (see partitioning result in *.json file). I wonder why there is such partition here? Are there any opportunities to construct the specific partitions in EQY?

I've attached an archive with Verilog descriptions, JSON result of partitioning and EQY config too.

Thanks in advance!

eqy_fail.tar.gz

[ssmolov]

I give a couple of details for this problem.
Here is the "gold" design named in1.v:

module Design_000159 (
  input in_6 ,
  input in_7 ,
  output out_11 ,
  output out_15
);
  wire one_16 ;
  wire zero_17 ;
  wire xor_18 ;
  wire and_19 ;
  wire xor_20 ;
  wire xor_41 ;
  assign one_16 = 1 ;
  assign zero_17 = 0 ;
  xor ( xor_18 , in_7 , one_16 );
  and ( and_19 , in_7 , one_16 );
  xor ( xor_20 , in_6 , zero_17 );
  xor ( xor_41 , and_19 , xor_20 );
  assign out_11 = xor_41 ;
  assign out_15 = xor_18 ;
endmodule // Design_000159

And here is the "gate" design named in2.v:

module Design_000159 (
  input in_6 ,
  input in_7 ,
  output out_11 ,
  output out_15
);
  wire one_16 ;
  wire zero_17 ;
  wire and_18 ;
  wire and_28 ;
  wire and_29 ;
  wire and_33 ;
  assign one_16 = 1 ;
  assign zero_17 = 0 ;
  and ( and_18 , in_7 , one_16 );
  and ( and_28 , in_6 , and_18 );
  and ( and_29 , ~and_18 , ~in_6 );
  and ( and_33 , ~and_28 , ~and_29 );
  assign out_11 = and_33 ;
  assign out_15 = ~in_7 ;
endmodule // Design_000159

The scenario for EQY is as follows:

[gold]
read_verilog in1.v
prep -top Design_000159

[gate]
read_verilog in2.v
prep -top Design_000159

[match Design_000159]
gold-nomatch and*
gold-nomatch xor*
gold-nomatch one*
gold-nomatch zero*

gate-nomatch and*
gate-nomatch one*
gate-nomatch zero*

[strategy sat]
use sat
depth 10

The checking result is as follows:

EQY 17:37:20 [script_sat] read_gold: starting process "yosys -g -ql script_sat/gold.log script_sat/gold.ys"
EQY 17:37:20 [script_sat] read_gold: finished (returncode=0)
EQY 17:37:20 [script_sat] read_gate: starting process "yosys -g -ql script_sat/gate.log script_sat/gate.ys"
EQY 17:37:20 [script_sat] read_gate: finished (returncode=0)
EQY 17:37:20 [script_sat] combine: starting process "yosys -g -ql script_sat/combine.log script_sat/combine.ys"
EQY 17:37:20 [script_sat] combine: finished (returncode=0)
EQY 17:37:20 [script_sat] Created ID database with 11 gold ids and 11 gate ids.
EQY 17:37:20 [script_sat] Matched 1 nets: [Design_000159] gold-nomatch and*
EQY 17:37:20 [script_sat] Matched 3 nets: [Design_000159] gold-nomatch xor*
EQY 17:37:20 [script_sat] Matched 1 nets: [Design_000159] gold-nomatch one*
EQY 17:37:20 [script_sat] Matched 1 nets: [Design_000159] gold-nomatch zero*
EQY 17:37:20 [script_sat] Matched 4 nets: [Design_000159] gate-nomatch and*
EQY 17:37:20 [script_sat] Matched 1 nets: [Design_000159] gate-nomatch one*
EQY 17:37:20 [script_sat] Matched 1 nets: [Design_000159] gate-nomatch zero*
EQY 17:37:20 [script_sat] Matched 4 nets: [*] gold-match *
EQY 17:37:20 [script_sat] partition: starting process "cd script_sat; yosys -ql partition.log partition.ys"
EQY 17:37:20 [script_sat] partition: finished (returncode=0)
EQY 17:37:20 [script_sat] Warning: Partition Design_000159.out_11 contains 1 unused gold inputs.
EQY 17:37:20 [script_sat] run: starting process "make -C script_sat -f strategies.mk"
EQY 17:37:20 [script_sat] run: make: Entering directory '/home/ssedai/samples/eqy/test_1_2/script_sat'
EQY 17:37:20 [script_sat] run: Running strategy 'sat' on 'Design_000159.out_11'..
EQY 17:37:20 [script_sat] run: Could not prove equivalence of partition 'Design_000159.out_11' using strategy 'sat'
EQY 17:37:20 [script_sat] run: Running strategy 'sat' on 'Design_000159.out_15'..
EQY 17:37:20 [script_sat] run: Proved equivalence of partition 'Design_000159.out_15' using strategy 'sat'
EQY 17:37:20 [script_sat] run: make -f strategies.mk summary
EQY 17:37:20 [script_sat] run: make[1]: Entering directory '/home/ssedai/samples/eqy/test_1_2/script_sat'
EQY 17:37:20 [script_sat] run: make[1]: Leaving directory '/home/ssedai/samples/eqy/test_1_2/script_sat'
EQY 17:37:20 [script_sat] run: make: Leaving directory '/home/ssedai/samples/eqy/test_1_2/script_sat'
EQY 17:37:20 [script_sat] run: finished (returncode=0)
EQY 17:37:20 [script_sat] Successfully proved equivalence of partition Design_000159.out_15
EQY 17:37:20 [script_sat] Warning: Failed to prove equivalence for 1/2 partitions:
EQY 17:37:20 [script_sat] Failed to prove equivalence of partition Design_000159.out_11
EQY 17:37:20 [script_sat] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
EQY 17:37:20 [script_sat] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
EQY 17:37:20 [script_sat] DONE (FAIL, rc=2)

When I dive into the counterexample, I found that for gate design the opt_merge Yosys pass detects A input for and_29 cell as identical to out_15. It is shown in gate.il:

  attribute \src "in2.v:17.6-17.35"
  cell $and $and$in2.v:17$5
    parameter \A_SIGNED 0
    parameter \A_WIDTH 1
    parameter \B_SIGNED 0
    parameter \B_WIDTH 1
    parameter \Y_WIDTH 1
    connect \A \out_15
    connect \B $not$in2.v:17$4_Y
    connect \Y \and_29
  end

After that, during equivalence checking, the out_15 is treated as primary input which results in wrong counterexample. As script_sat/strategies/Design_000159.out_11/sat/run.log states, both in_7 and out_15 should have same results:

 Time Signal Name                               Dec       Hex                                 Bin
  ---- --------------------------------- ----------- --------- -----------------------------------
     1 \__pi_in_6                                  0         0                                   0
     1 \__pi_in_7                                  0         0                                   0
     1 \__pi_out_15                                0         0                                   0
     1 \__po_out_11__assert.i                      1         1    00000000000000000000000000000001
     1 \__po_out_11__assert.in_gate                1         1                                   1
     1 \__po_out_11__assert.in_gold                0         0                                   0
     1 \__po_out_11__assert.okay                   0         0                                   0
     1 \__po_out_11__gate                          1         1                                   1
     1 \__po_out_11__gold                          0         0                                   0
     1 \gate.__pi_in_6                             0         0                                   0
     1 \gate.__pi_in_7                             0         0                                   0
     1 \gate.__pi_out_15                           0         0                                   0
     1 \gate.__po_out_11                           1         1                                   1
     1 \gate.and_18                                0         0                                   0
     1 \gate.and_28                                0         0                                   0
     1 \gate.and_29                                0         0                                   0
     1 \gate.in_6                                  0         0                                   0
     1 \gate.in_7                                  0         0                                   0
     1 \gate.out_11                                1         1                                   1
     1 \gate.out_15                                0         0                                   0
     1 \gold.__pi_in_6                             0         0                                   0
     1 \gold.__pi_in_7                             0         0                                   0
     1 \gold.__pi_out_15                           0         0                                   0
     1 \gold.__po_out_11                           0         0                                   0
     1 \gold.and_19                                0         0                                   0
     1 \gold.in_6                                  0         0                                   0
     1 \gold.in_7                                  0         0                                   0
     1 \gold.out_11                                0         0                                   0
     1 \gold.out_15                                0         0                                   0
     1 \gold.xor_20                                0         0                                   0
Dumping SAT model to VCD file trace.vcd

It is impossible (see last "assign" in gate design). I've removed "prep" pass from *.eqy and equivalence checking returned "OK", but it looks that is some cases "opt_merge" pass may break the circuit in a non-equivalent way.