It is quite common to see LEC (Logic Equivalency Check) failures due to undriven nets in the RTL. Any new comer trying to prove logic equivalence between RTL and gates need to be aware of how to handle undriven nets. The examples and snapshots in this article are put forth based on the observations while using Cadence Conformal LEC tool but the underlying concept can also be applied for any other logic equivalence check tool like Synopsys’s Formality. LEC failures occur due to the fact that we guide the synthesis and LEC tools to model these undriven signals differently.
What are the reasons for undriven signals in RTL ?
Undriven signals are the floating signals in the RTL which do not have any drivers. Often these undriven signals end up in RTL due to incomplete code. In reality any net in our design can be at one of the two logic values (0 or 1). However there is no harm in having undriven nets in the design unless the logic to which it is connected to does not contributing to the design functionality (dead logic).
Code showing incomplete port mapping for an sub_design instance,
module top_design( b, s0, a, y ); input b; input s0; input a; output y; wire b; wire s0; wire a; wire y; sub_design sub_design_inst ( .A(), .B(b), .S0(s0), .Y(y)); endmodule
sub_design is a two input multiplexer and it’s RTL code is,
module sub_design( B, S0, A, Y ); input B; input S0; input A; output Y; wire B; wire S0; wire A; wire Y; assign Y = (S0)?A:B; endmodule
How synthesis tools model undriven signals ?
Some synthesis tools model these undriven signals based on the user controls. If you are using Cadence tools like RC compiler or Genus then it depends on the following attribute setting,
set_attribute hdl_undriven_signal_value <0|1|x|none>
Synopsys’s Design Compiler tool would by default tie undriven nets to ground. Modeling the undriven nets to either 0 or 1 allows the tool to optimize the logic in it’s fanout. In synthesis, it’s quite common to direct the tool to optimize the undriven nets assuming it is grounded for better area.
Snippet showing the undriven pin has been tied low in the the gates,
module top_design(b, s0, a, y); input b, s0, a; output y; wire b, s0, a; wire y; sub_design sub_design_inst(.B (b), .S0 (s0), .A (1'b0), .Y (y)); endmodule module sub_design(B, S0, A, Y); input B, S0, A; output Y; wire B, S0, A; wire Y; and g2 (Y, B, wc); not gc (wc, S0); endmodule
Since the undriven pin “A” of sub_design is tied to 1’b0, the logic inside the sub_design is also optimized. If we see the schematic of the top_design after synthesis in Conformal LEC, it would look like the one in the picture below. This is what we usually call it as the revised side of the Logic Equivalence Check.
How Conformal LEC models undriven signals ?
Logic Equivalency Check tools models the undriven nets in High impedence state (open circuit) which is the reality. Unlike synthesis tools it does not assume undriven signals as grounded. This is the expected behavior of any Logic Equivalency check tools who’s purpose is to catch such deviations in logic other than what is coded in the RTL.
Schematic view of how the top_design would be modeled in the LEC is shown in the picture below. This is otherwise called as the golden side of the Logic Equivalence Check.
How to identify undriven nets in LEC?
One of the early indicators of the RTL containing undriven nets is incomplete mapping. This is because the LEC tools tries to map undriven nets modeled as “tiez” in RTL to a corresponding “tiez” in the gates. Since synthesis tools optimize them away, the LEC tool cannot find a corresponding mapping key point. Command to report unmapped points of type Z (tiez) in vpxmode is,
report unmapped points -type z
The result of this command if applied on our example above would show us,
Unmapped point (not-mapped): (G) 5 Z /sub_design_inst/A 1 unmapped points reported ================================================================================ Golden: -------------------------------------------------------------------------------- Unmapped points Z Total -------------------------------------------------------------------------------- Not-mapped 1 1 ================================================================================
These undriven nets are no harm if they do not contribute to the functionality of the design. In other words these undriven nets does not cause any failures if they only exist in the fan in cone of unreachable flops (dead logic). Discussions on the unreachable flops is beyond the scope of this article.
To know if the undriven nets in the RTL cause LEC failures, one can take a look at the Non-equivalent points report using the command,
analyze nonequivalent <gate_id> -verbose
The result of this command when applied for our example design would look like,
Analyzing non-equivalent compared points: (G) + 4 PO /y (R) + 4 PO /y Support in Golden has unbalanced Z gates. Analysis of non-equivalent compared points: Unmapped Z gate in supports. (Occurrence: 1)
From the report above straight away assume that undriven nets in RTL as the reason for failure.
Right approach in resolving the non equivalents due to undriven nets in RTL:
After we determine that undriven nets in the RTL cause LEC failures we need to make sure that undriven nets in the RTL are the only reason for the failure and nothing else. How can we do that ? This can be achieved by guiding the LEC to follow what synthesis tool has done for the undriven nets (tie them to ground). In Conformal LEC following command guides tool to treat the undriven nets as grounded (similar to the synthesis tool behavior. It’s very rare that we guide synthesis tools to tie undriven nets to 1’b1 unless there is a special reason as communicated by the designer) .
set undriven signal 0 -golden
Schematic of top_design after the above command would look like,
After this we can run compare to check if there are any non equivalent points reported. If there are no non equivalent points reported, then we can make sure that there are no other issues. If there are non-equivalent points, then you can proceed to debug the other reasons for the failures. In any case it is very important to report these undriven nets as a feedback to the designer so that he can either tie those undriven signals to known value of (either 1 or 0). You can get the list of undriven nets from the LEC tool so that you can pass on this info to the designer using the command,
report unmapped points -type z
*Remember that you need to get this report from the LEC session where you have not set undriven signals to 0 in the golden side.