Altera recommends using the following guidelines when synthesizing a design using Integrated Synthesis and then perform formal verification using the Encounter Conformal software. These guidelines help prepare the design for formal verification and help prevent mismatches or unmapped points when comparing the original RTL-level netlist with the -generated gate-level netlist.
Use the following guidelines when creating the VerilogHDL or VHDL design in the software:
Synthesis directives or pragmas have limited support in the Encounter Conformal formal verification tool. The <design name>.ctc script file, which is used to perform formal verification with the Encounter Conformal software, disables any unsupported synthesis directives generated by the EDA Netlist Writer.
Integrated Synthesis converts megafunctions or library of parameterized modules (LPM) functions without a formal verification model to black box entities. The formal verification models provided for the Encounter Conformal software are located in the /< system directory>eda/fv_lib/<verilog or vhdl>/ directory. Altera recommends creating black box entities for any megafunctions or LPM functions in the design without a formal verification model.
The software lists any megafunctions or LPM functions converted to black box entities in the Automatically Created Black Box Entities report.
The software automatically recognizes RAM and infers the appropriate megafunction, if the Auto RAM Replacement logic option is turned on. However, inferred RAM instances are not supported by the Encounter Conformal software. Therefore, Integrated Synthesis treats the entire entity containing the respective instance as a black box entity. As a result, the entire entity (not just the RAM logic) cannot be verified by the Encounter Conformal software. Altera recommends creating the RAM logic as a black box to minimize the amount of logic treated as a black box entity. You can also use the IP Catalog to directly instantiate a megafunction.
ROM and shift register instances are not inferred because they would be implemented using memory blocks which cannot be verified by the formal verification tool. Consequently, the Auto ROM Replacement logic option and the Auto Shift Register Replacement logic option are ignored when they are selected together with a valid formal verification tool. This may have an impact on the area of the design. However, ROM and shift register instances can be verified. You can limit this impact by instantiating ROM or shift register logic explicitly, or by declaring the entity containing the ROM or shift register as a formal verification black box.
Integrated Synthesis automatically infers latches from some HDL constructs that result in combinational loops in the design. However, Integrated Synthesis and the Encounter Conformal software may implement these latches differently, which may lead to formal verification mismatches. Altera recommends reducing latch use in the design, or using the MegaWizard Plug-In Manager to instantiate the lpm_latch megafunction.
The software lists latches in the Detected Latches Section of the Report window.
Both Integrated Synthesis and the Encounter Conformal software recognize and encode state machines, however, they may encode state machines differently. If no state machine encoding is specified, Integrated Synthesis uses the best suited encoding, while Encounter Conformal uses sequential encoding. The software writes the encoding relation between Integrated Synthesis and the Encounter Conformal software to a <project name>.<state machine number>.fsm file in the /<project directory>/db/ directory (one for each state machine) and directs the Encounter Conformal software to recognize the encoding relationship in the <design name>.ctc script file.
The software lists each state machine, its state values, and its bit values in the State Machine Encoding report.
Combinational loops may result in mismatches when performing formal verification. However, Integrated Synthesis represents combinational loops as logic cells in the design, but does not communicate this representation to the Encounter Conformal software. You must add the logic cell in the form of a cut point to the <design name>.ctc script file. In general, Altera recommends eliminating combinational loops in the design by inserting registers in the feedback loop.
The software reports the combinational loop and the signal driving the logic cell in the Logic Cells Providing Combinational Loops for Formal Verification report.
The Encounter Conformal software compares the behavior of each sequential node in the design. However, if an inversion is pushed through a register and implemented on the data input (NOT gate push-back), the value of the data input for the node is inverted, and the Encounter Conformal software may report an inverted equivalent signal. These registers are automatically added to the <design name>.ctc script file.
The software reports any inverted registers in the Register Inversion report.
Integrated Synthesis removes registers with values stuck at GND or VCC and adds a commented-out command to the <design name>.ctc script file that informs the Encounter Conformal software that the register was removed. You can uncomment the command in the script file after verifying that the register value is correct, making sure that the value does not create any other errors for the design in the Encounter Conformal software. Altera recommends verifying that each register with a value stuck at GND or VCC is intentional and that removing the register is correct before notifying the Encounter Conformal software. If these registers values are unintentional, Altera recommends recoding the design to remove the registers stuck and GND or VCC.
The software reports all removed registers with values stuck at GND or VCC in the Registers Stuck At GND or VCC report.
Integrated Synthesis may merge duplicate registers to optimize the area of a design or Integrated Synthesis may duplicate registers (for example, if you specified the Maximum Fan-Out logic option on a register, pin, or logic cell buffer, and the software duplicated registers as a result). The software writes this information to the <design name>.ctc script file, informing the Encounter Conformal software that the registers were duplicated or merged, to eliminate potential mismatches during formal verification.
The software lists information about the merged or duplicated registers in the Merged Registers and Duplicated Registers reports.