logic equivalence check

[rabia1234-eng]

I am currently working on a verification task involving LEC (Logical Equivalence Checking) using Formality. Unfortunately, I have encountered a verification failure in this process. The focus of this verification task is to compare the RTL (Register Transfer Level) design with the netlist. The netlist has been generated after synthesizing a specific block using the Fusion Compiler.The issue I am facing appears to be located within the FC_CORE portion of our design. The verification failure is primarily attributed to unmatched inputs or required input mismatches between the RTL and the synthesized netlist.

I am seeking help from anyone with expertise in logic equivalence checking or experience with similar verification tasks. If there is someone who can assist with debugging or provide insights into resolving this issue, your assistance would be greatly appreciated.

[bluewww]

The only IP that we needed to exclude from LEC (by blackboxing it) was the FPU. All LEC tools struggled with it resulting in timeouts. Other than that, RTL <-> netlist LEC passed just fine.

Also without more detailed information about the problem you are facing we cannot really help.

[rabia1234-eng]

can you please share the scripts of LEC passing RTL vs netlist so that I can review the constraints , if not then can you please discuss what are the constraints/app_options needed for LEC

[bluewww]

Unfortunately I'm not allowed to share those scripts. As I said previously, you just need to blackbox the FPU (module fpnew_top). Your tools' manual should explain how to do this.

[rabia1234-eng]

Thank you but I've already treated it as a black box. My inquiry pertains to whether there are additional constraints beyond those related to the black box IP. However, despite this approach, I'm encountering lots of verification failures let's discuss one of them

Ref DFF r:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_
Impl DFF i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

issue is :

fm_shell (verify)> analyze_points r:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_re g_0__0_
Found 3 Unmatched Cone Inputs

Unmatched cone inputs result either from mismatched compare points
or from differences in the logic within the cones. Only unmatched
inputs that are suspected of contributing to verification failures
are included in the report.
The source of the matching or logical differences may be determined
using the schematic, cone and source views.

r:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/u_mux_ioss_clk/tsmc_mux_UDP_01/p1
Is globally unmatched affecting 1 compare point(s):
i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/clock_gate_mhpmcounter_q_reg/*lat.00*
Is globally unmatched affecting 1 compare point(s):
r:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

i:/WORK/ioss_wrap/ref_clk_i
Matched with port r:/WORK/ioss_wrap/ref_clk_i
Exists in the impl cone but not in the ref cone for 1 compare point(s):
r:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

---

Found 5 Required Inputs

A required input is one that is designated as required
for all failing patterns for one or more cpoints and fans out
to more failing than passing points.
This implies that it may be driving downstream logic that is related to
the failure(s)

i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mcountinhibit_q_reg_0_/*dff.00*
Fans out to 141 failing and 0 passing points and has
logic value '1' for 1 compare point(s):
i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/soc_peripherals_i/i_apb_soc_ctrl/r_crg_rego_reg_0_/*dff.00*
Fans out to 34911 failing and 5404 passing points and has
logic value '1' for 1 compare point(s):
i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

i:/WORK/ioss_wrap/dft_test_mode_i
Fans out to 36705 failing and 0 passing points and has
logic value '1' for 1 compare point(s):
i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

i:/WORK/ioss_wrap/ref_clk_i
Fans out to 34610 failing and 1 passing points and has
logic value '0' for 1 compare point(s):
i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

i:/WORK/ioss_wrap/rstn_glob_i
Fans out to 34926 failing and 5407 passing points and has
logic value '1' for 1 compare point(s):
i:/WORK/ioss_wrap/u_io_subsys_wrapper/u_ioss/fc_subsystem_i/FC_CORE_FC_CORE_i/cs_registers_i/mhpmcounter_q_reg_0__0_

---

---

---

Analysis Completed
1