Altera recommends using the following guidelines when synthesizing a design using Quartus II 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 Quartus II-generated gate-level netlist.
Use the following guidelines when creating the Verilog HDL or VHDL design in the Quartus II software:
-
Limit use of synthesis directives or pragmas
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.
-
Convert entities without formal verification models to black box entities
Quartus II 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 /<Quartus II 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 Quartus II software lists any megafunctions or LPM functions converted to black box entities in the Automatically Created Black Box Entities report.
-
Convert inferred RAM instances to black box entities
The Quartus II software automatically recognizes RAM and infers the appropriate megafunction, if the logic option is turned on. However, inferred RAM instances are not supported by the Encounter Conformal software. Therefore, Quartus II 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 MegaWizard Plug-In Manager to directly instantiate a megafunction.
-
ROM and shift register instances as black box entities
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 logic option and the 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.
-
The Quartus II software lists the inferred RAM, ROM, and shift register instances in the following reports:
-
Suggested RAM Megafunction or Black-Box Entity Section
-
Suggested ROM Megafunction or Black-Box Entity Section
-
Suggested Shift Register Megafunction or Black-Box Entity Section
-
Reduce latch use
Quartus II Integrated Synthesis automatically infers latches from some HDL constructs that result in combinational loops in the design. However, Quartus II 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 Quartus II software lists latches in the Detected Latches Section of the Report window.
-
Specify State Machine Encoding
Both Quartus II 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, Quartus II Integrated Synthesis uses the best suited encoding, while Encounter Conformal uses sequential encoding. The Quartus II software writes the encoding relation between Quartus II 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 Quartus II software lists each state machine, its state values, and its bit values in the State Machine Encoding report.
-
Logic cells representing combinational loops
Combinational loops may result in mismatches when performing formal verification. However, Quartus II 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 Quartus II software reports the combinational loop and the signal driving the logic cell in the Logic Cells Providing Combinational Loops for Formal Verification report.
-
Register inversion
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 Quartus II software reports any inverted registers in the Register Inversion report.
-
Registers stuck at GND or VCC
Quartus II 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 Quartus II software reports all removed registers with values stuck at GND or VCC in the Registers Stuck At GND or VCC report.
-
Merged or Duplicated Registers
Quartus II Integrated Synthesis may merge duplicate registers to optimize the area of a design or Quartus II Integrated Synthesis may duplicate registers (for example, if you specified the logic option on a register, pin, or logic cell buffer, and the Quartus II software duplicated registers as a result). The Quartus II 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 Quartus II software lists information about the merged or duplicated registers in the Merged Registers and Duplicated Registers reports.
Literature
> 
