Failing Supplemental LEC (Logical Equivalence Checking)

[Peter-Herrmann]

If the LEC checks are enabled using LEC_ENABLE, there are 2 instances of equivalence that cannot be proven after Running Global Routing Resizer Timing Optimizations. Note that these checks are not required, and only being done as a supplemental check.

The two instances are:

  Trying to prove $equiv cell $auto$equiv_make.cc:369:find_same_cells$81699:
    A = \_40836_.B, B = \i_core.i_imem_obi_driver.PS, Y = \_41296_.B
    Adding 6631 new cells to the problem (6631 A, 2 B, 2 shared).
    Problem size at t=10: 30356 literals, 76474 clauses
    Failed to prove equivalence with sequence length 0.
    No nets to continue in previous time step.
	
  Trying to prove $equiv cell $auto$equiv_make.cc:369:find_same_cells$81701:
    A = \i_core.i_imem_obi_driver.PS, B = \_40836_.B, Y = \_41296_.A
    Adding 6631 new cells to the problem (2 A, 6631 B, 2 shared).
    Problem size at t=10: 30356 literals, 76474 clauses
    Failed to prove equivalence with sequence length 0.
    No nets to continue in previous time step.

i_core.i_imem_obi_driver.PS is the present state value for a Mealy-type FSM. There are two instances of this FSM, i_imem_obi_driver and i_dmem_obi_driver. Only the former is failing logical equivalence checking, and the only significant difference between the instances is that two of the ports are tied to constant values:

    obi_req_driver i_imem_obi_driver (
        .clk_i,
        .rst_ni,

        .rd_i     ('1),
        .wr_i     ('0),

        .gnt_i    (imem_gnt_i),
        .rvalid_i (imem_rvalid_i),

        .stall_o  (imem_stall),
        .req_o    (imem_req_o)
    );

    obi_req_driver i_dmem_obi_driver (
        .clk_i,
        .rst_ni,

        .rd_i     (dmem_rd),
        .wr_i     (dmem_wr),

        .gnt_i    (dmem_gnt_i),
        .rvalid_i (dmem_rvalid_i),

        .stall_o  (dmem_stall),
        .req_o    (dmem_req_o)
    );

A manual review of the FSM definition in obi_req_driver did not identify any problems that might cause ambiguity in the implementation.