search

pulp-platform / pulp_soc

pulp_soc is the core building component of PULP based SoCs
Other
78 stars 81 forks source link

logic equivalence check #93

Open rabia1234-eng opened 12 months ago

rabia1234-eng commented 12 months ago

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 commented 12 months ago

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 commented 12 months ago

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 commented 12 months ago

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 commented 12 months ago

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_reg0/*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_reg0/*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