Pitfalls for Logical Equivalence Check

Preeti Agarwal, Abhishek Mahajan & Gaurav Goyal (Freescale Semiconductor)

The VLSI design cycle is partitioned into two phases i.e. front-end and back-end phases of the complete SoC design cycle. While at front-end, most of the architectural specifications, coding and verification parts are performed; similarly back-end involves more with the physical implementation of the design on the targeted technology node. The register transfer level (RTL) behavior of a chip is usually described by the hardware description languages such as Vhdl, verilog. This description is the golden reference model that describes in detail which operations are to be executed. The RTLs are then synthesized to produce a logical Netlist using the standard cells of targeted technology node and all the design parameters.

Once the logic designers, by simulations and other verification methods, have verified register transfer description, the design is usually converted into a gate level netlist by the logic synthesis technique. This netlist undergoes many optimizations, with the addition of DFT structures. Significant modifications such as replacing logic elements with equivalent elements are also done. But it is very much important that throughout the process the original functionality of the code must be maintained. A logic synthesis tool guarantees that the netlist is logically equivalent to the RTL source code. LEC (Logic Equivalence Check) is the essential step to ensure the functional check between RTL and netlist as can also be depicted from the Fig. 1. Many EDA companies provide tools to do the check. A logical equivalence check can be performed between any two representations of a design: RTL vs Netlist or Netlist vs Netlist.

Fig. 1 Basic IC Design Flow

The necessary inputs needed for the LEC are being discussed in the paper and if they are not taken care of properly then adverse consequences could be seen and also SoC could fail at the customer end as it would be a clear mismatch between the desired and the delivered patterns and it is a complete waste of engineering time. There are several inputs required for the LEC but some are very crucial and sometimes generally overlooked which have been discussed below:

Robust Black Box modeling.
Correct Scan constraints.
Port mismatch between Timing model & behavioral code.

1. Robust Black Box modeling:

During synthesis, there are several analog-IP, memory blocks, and pads etc which are not meant to be synthesized. Their model (library/lef) needs to be picked during the synthesis. It is essential to use the exhaustive list of Black-Box modules in LEC setup as these are the modules which don’t require internal verification but their interface has to be exhaustively checked so as to confirm their interaction with rest of the design.

If any module is missed from this list of all the black-boxes in the design and if there is any interaction between this module with other part of the SOG then LEC tool will not check for such interactions, which sometimes misses the genuine non-equivalencies like broken connections between these interacting modules. For e.g. REV-ID are used in the design to check the revision of the silicon.

Fig. 1.1 Black Box modeling for LEC

Refer to Fig 1.1 Here on the Golden side 0th bit of REV-ID is muxed with some signal and goes to padring. Now if during synthesis, the last bit of REV-ID propagates in the design & the connection between last bit of REV-ID and B input of mux is now broken and this B input will now be connected to 1’b0. Because of this, it’s not possible to do the change in the REV-ID cell during the revision of the chip and the purpose of using REV-ID is also defeated. Now in LEC, if REV-ID is missed from the Black-box module list, tool will not report any non-equivalencies. But if REV-ID is added to the black-box modules list, non-equivalencies will be reported due to the broken link between 0th bit of REV-ID and B input of mux. So, to avoid all such cases, it is mandatory to have the complete list of all the Black-Boxes.

2. Correct Scan constraints:

The goal of scan design is to make a difficult-to-test sequential circuit behavior (during the testing process) like the way an easier-to-test combinational circuit. Achieving this goal involves replacing sequential elements with scan able sequential elements (scan cells/scan flops) and then stitching the scan cells together into scan registers, or scan chains. These serially connected scan cells can then be used to shift data in and out when the design is in scan mode.

“Before Scan” design is difficult to initialize to a known state, making it difficult to both control the internal circuitry and observe its behavior using the primary inputs and outputs of the design. In a "Scan design" scan memory elements (scan flops) replace the original memory elements (normal flops) imparting controllability and observability to the design (prime requirement for the design being testable), when shifting is enabled. For LEC between functional vs scan design, these controllable points need to be constrained to do the functional check. To check the faults on the reset pin of the flops, they are also made controllable from the top level during scan stitching. For LEC check between functional vs scan stitched netlist, there is a need to provide constraints for the scan stitched netlist which will bypass the connections made during the scan stitching and were not present there in the RTL. So, to do the LEC check, it is mandatory to constraint such observable points.

Fig. 2 A Typical scan path after scan stitching.

There should not be any changes at scan ports as while doing the LEC between functional v/s scan stitched design, these ports are constraints to their respective values due to which these scan ports are bypassed and if any change in design at these scan ports are not implemented properly because of some manual error, then these non-equivalency will not be caught by the tool. Hence, such changes at the scan ports must be avoided. In Fig. 2, the TE pin is constrained to 1’b1 so as to get into the scan mode and to 1’b0 to get into functional mode. If there is some ECO on this TE pin, then there is no way in LEC to check that implemented change as during the LEC check, there is a need to constraint this signal to 1’b0 which will mask the logic behind it and ECO cannot be checked.

There should not be any scan input in the design connected to functional logic as during LEC, this scan input will be constrained which will bypass the functional logic connected to this scan input due to which the logic connected to this scan input will not be checked by the tool and tool might miss genuine non-equivalencies.

Fig. 3 A Typical scenario for any SoC.

In fig. 3, In RTL, a logic box has a scan input which is connected to functional logic by A. Now after scan stitching, logic box will be connected to the other flops as well as shown in the fig. 3. During LEC, this scan input would be constrained which will bypass the connection between the logic box and ‘A’ input and the hence the logic connected to it will not be checked by the tool.

All the scan enables need not be constrained in LEC. Only those scan enables are to be constrained which were not connected in RTL. Only then we can have a correct list of scan-constraints.

3. Port mismatch between Timing model & behavioral code:

There are models which have timing information of the block in any hierarchical design. In complex SOC, advance synthesis approach is followed in which the synthesis of the blocks is done separately. But there can be some interaction between the rest of the design and these synthesized blocks.

So, the paths between them need to be timed. Timing model (PTM) provides such timing information. There should be proper PTM generation. Inputs and outputs defined in PTM must match with that in RTL verilog model of that partition.

Fig. 4 A Typical SoC depicting Partitions A, B & C.

Any mismatch in the direction of the pins in verilog model and PTM results in optimization of the undesired logic during synthesis and results in non-equivalence in LEC. Refer Fig. 4, here in SoC, we have three partitions. We want to synthesize these partitions separately. But for top-level synthesis, we need timing information of these blocks. So we generate PTM that has timing information of these blocks. In the fig 4., arc “ab” and arc “ac” are defined in the PTM. So we give PTM as an input to synthesis tool to do the timing optimizations for the top design. In verilog code port B is defined as a input port. Now if by any human error, port B is defined as output port in PTM. Due to this mismatch, tool will optimize this port, which may cause optimization of the logic connected to this port and hence results in optimization of the undesired logic. Hence this thing needs to be taken care during the generation of PTM.

Conclusion:

From the above discussion, it is quite clear that it is very much important to incorporate the above discussed best design practices and should not let them overlooked so as to have robust Silicon.

Acronym