Leveraging Symbolic Simulations For IO Verification

The complexity of interface IP makes it a challenge to keep transistor netlist views logically equivalent to reference Verilog models.


IO libraries and interface IPs are an important part of any integrated circuit design that needs to communicate with the outside world or other integrated circuits. Interface IPs are the literal gatekeepers to the flow of logical and electrical information from one IC to another to form today’s complex computer systems, influencing almost every aspect of our lives these days. Interface IPs (e.g., PCI Express, HDMI, USB, DDR, Bluetooth, Ethernet, etc.) provide high throughput, low latency, and energy-efficient device-to-device external connectivity for systems on chip (SoCs) in mobile, AI, cloud computing, networking, storage, and automotive applications. While these interface protocols open gates to connect different compute systems, their complexity brings a vast amount of verification challenges. Out of many design views of IO libraries, the logical views have special importance. Logical models define the basic function of the design. If not verified to the best possible extent, it can fail to perform the very basic task for which an IP was designed in the first place. Broken functionality leads to one of the heaviest costs a design house may pay in terms of silicon failures.

The equivalence challenge

With tremendous advances in digital synthesis and related formal equivalence checkers in the past several decades, even the most complex and sophisticated digital designs can be verified for logical equivalence between Verilog models and gate-level netlists nearly automatically. Formal methods of logic equivalence checkers hold tremendous power when it comes to verifying logical Verilog models against gate-level netlists that eventually make it to silicon. The kind of coverage and speed advantage they bring are best appreciated by designers that make use of these formal methods. However, netlist views of custom circuits like interface IPs are hand-crafted transistor-level netlists. Almost the entire interface IP is designed placing one transistor at a time manually. In the absence of synthesized models, the netlist views of custom circuits don’t have the luxury of using traditional formal methods. With the complex functions these custom IPs perform, it’s a big challenge to keep these transistor netlist views logically equivalent to reference Verilog models. One of the traditional ways to cross-check the functionality of the SPICE netlist model against the reference Verilog model is to make use of binary simulations using hand-crafted binary vectors. However, to design complete and sophisticated binary vectors requires a deep understanding of the design from a logic function point of view. With interface IPs performing very complex functions at IO ports, and IO ports being subjected to intricate function modes of gatekeeping data in either direction, it’s extremely hard and error-prone to keep binary vectors up-to date with ever-changing logic function requirements of modern interface IPs. Moreover, it’s even harder to predict the kind of real-world scenarios to which an IP would be subjected, leaving binary simulation methods incomplete in nature. Other than the challenges of covering the entire design space for function equivalence checks, it’s a very time-consuming task to design and run binary vectors for SPICE netlists. Even with fast SPICE simulators, it can take several hours (if not days) to run binary SPICE simulations to simulate modern intricate IO designs. Long runtimes also add to debug challenges as any design update would require a long runtime before its logic effect can be measured and validated. This becomes even more challenging if design updates are made closer to tape-out dates.

Symbolic simulation to the rescue:

  • Vector independent verification: A vector independent symbolic simulation overcomes all the challenges imposed by traditional binary simulation approaches. Binary simulation vectors are handcrafted by CAD and design teams, however a symbolic simulator relies on auto-generated symbolic vectors that cover all binary vectors in just a fraction of simulation cycles.
  • Maximum verification coverage: Symbolic simulation provides best of class coverage at the shortest simulation runtimes possible. Traditionally, verification coverage is dependent upon binary vectors. However, since the symbolic simulator relies on its own symbolic vectors that automatically cover the entire Boolean logic space, a symbolic simulation provides the best verification coverage.
  • Shortest simulation runtime: Traditionally, coverage comes at the cost of runtime, but not with the symbolic simulation approach. Usually, a large number of binary vectors are run on a SPICE netlist using SPICE simulators for logic verification, which is a time-consuming process. Since a symbolic simulator covers the entire Boolean logic space using symbols, it needs just a fraction of the cycles. A set of binary simulations that can take hours or days can be completed with symbolic simulation in under a few minutes for the most complex interface IPs.
  • Less dependence on design knowledge: A symbolic simulation overcomes the requirement to have a deep understanding of the design and its functional specifications. Vector independent symbolic simulation goes one step further and tests the designs for real-world scenarios that may not have been thought through while designing traditional binary vectors.
  • Sequential vector capability: A modern IP runs under a lot of different modes. Traditionally, logic verification doesn’t cover all combinations of mode switching based on binary simulations. It’s missed primarily because the verification engineer may not have thought through all combinations of mode switching for real-world scenarios. The symbolic simulator does that automatically.
  • Most robust power-up verification: A binary simulator starts with random initialization of internal nets. Thus, no matter how many binary vectors one runs, the initial state of internal nodes is almost always set to a fixed combination. However, in the real-world, internal nets in a design (especially storage nodes) could initialize to different values based upon different process-voltage-temperature (PVT) conditions. This vast possibility of different combinations of internal design modes at power-up could lead to serious issues, resulting in silicon failures. The symbolic simulator can easily catch such issues as even internal net nodes can be provided with the possibility to seed all possible Boolean combinations using a symbolic simulator.

Symbolic simulation technology

In symbolic simulation, a design under test is subjected to logic symbols as inputs to input ports rather than binary logic_1 and logic_0. A logic symbol assumes both logic_1 and logic_0 values. A logic symbol can also be set to assume X and Z logic values. Once a logic symbol is applied to all inputs, a logic simulator computes the Boolean function of the design and propagates Boolean equations to design output ports. A Boolean equation at the design outputs port is a complete, functional representation of the design under test for every output port. For example, as shown in figure 1, a symbolic simulator would read the SPICE netlist AND gate and translate the transistor connectivity from SPICE netlist into its Boolean functional equation. A Boolean functional equation represents all possible input vectors for these two-input AND gate. The symbolic simulator also translates the Verilog model into its Boolean equation representation. Once functional equations for the Verilog model and SPICE netlist are computed, the simulator uses formal mathematical methods to prove the functional equivalence of two equations. Once equivalence is established by formal symbolic simulation methods, the two designs under test are considered an exact replica of each other from a logic function point of view.

Fig. 1

For a design that consists of a larger number of devices, a Boolean equation representation of its SPICE netlist would look like Figure 2.

Fig. 2

Each output port would bear a symbolic equation that has the complete information of the logic design for the entire logic path from primary input to a primary output. The feedback loops within the design are automatically captured by the tool to compute symbolic equations that capture the essence of these feedback loops. No matter how complex the design connectivity or how many different transistors are connected to form a SPICE netlist, a symbolic simulator can always translate a netlist into its Boolean functional equation for each output port. If the symbolic simulator is not able to establish formal functional equivalence during the mathematical comparison of Verilog and SPICE Boolean equations, then it intelligently creates a binary vector that can prove mismatch in behavior, run a binary simulation and dump waveforms to show the difference in behavior for two models under test. An automatic and controlled binary simulation of just a handful of cycles proves very efficient for designers to debug the root cause of mismatch in behavior between two models under test. A complete symbolic simulation of most interface IPs can be completed within a few minutes, thus providing maximum design coverage at the fastest speed possible.

Bonus value of symbolic coverage

Now that we have seen how a symbolic simulator can cover the entire functionality of two designs under test at best possible simulation runtimes and maximum coverage, let’s see how it goes a step beyond to uncover design discrepancies that can slip by the traditional binary simulation approach and manifest itself as silicon failure in real-world environments. Modern interface IPs have to cater to the ever-growing, complex real-world environments in which we use our devices (e.g., mobile, enterprise computing resources, automotive, AI, and cloud computing applications). It’s extremely difficult, if not impossible, to predict all possible binary vectors that can not only test a design under one mode but also how a design behaves when it changes gears from one mode of operation to another. Even product engineers who envision a product can’t completely predict the environment under which their designs will be used in the real world. When IPs are moving from one mode of operation to another, it’s extremely important for the SPICE netlist (or silicon) to behave exactly as Verilog models which were used to design and integrate SoCs for the SoCs to work as expected under all modes of operation. A symbolic simulator overcomes this huge challenge with its unparalleled reach in verifying logic sequences automatically, without having any deep understanding of the design. A Boolean equation represents a logic function of the design for a given cycle. However, if one runs multiple symbolic cycles, then each cycle represents a complex switching from one mode of operation to another mode of operation.

Fig. 3

This is one of the most powerful features of a symbolic simulator. It not only establishes the complete equivalence of two models under test, it also automatically delivers unmatched sequential mode transition check without writing a single hand-crafted binary vector.

Another very advanced and powerful feature of symbolic simulation is its unique capability to catch power-up issues. Based upon several PVT factors, internal design nodes, especially state-nodes, may power up to random logic states. These random logic states can sometimes conflict with each other causing logic or power-ground short issues at power-up. Such scenarios can even lead to locked up internal loops such that the deadlock can’t be removed within the scope of the design, thus leaving the entire silicon useless. Such silicon failure costs are catastrophic to say the least. A symbolic simulator has the capability to seed internal nets in such a way that all possible power-up combinations of these internal nets can be tested. A symbolic simulator can initialize and test all power-up scenarios within a single simulation comprising of a handful of simulation cycles.

Low power robustness

Though a functional equivalence check is the most basic check an interface IP needs to go through, there are more ways in which a symbolic simulator can increase the robustness of designs. With ubiquitous handheld devices and their need to communicate internally and with the outside world via wireless communication channels, low power consumption of every block on an integrated circuit is more important than ever – IOs or interface IPs are no different. While interface IPs need to provide seamless functional capabilities, they also need to operate at multiple voltages as signals flow from lower voltage cores to higher voltage interfaces and vice versa. Today’s complex IOs cater to these very complex power modes of operation for power management as well as basic functionality. With these complex power management and power modes of operation, it becomes very critical to catch low power issues. Some examples of some of these power issues (e.g., missing level shifters, power-round shorts, sneak paths, undriven gates, etc.) are shown in figure 4.

Fig. 4

These non-CMOS logic-related power/ground issues could be present lower down the hierarchy in a design and very hard to catch with the traditional binary vector approach as the binary vector required to manifest the issue may never have been applied. Traditionally, a designer needs to handcraft meticulous binary vectors to unearth hidden and corner case low power issues. Since a symbolic simulator is not dependent upon the user to create its vectors, and symbolic Boolean equations on every net of the netlist have complete information about a functional scenario under which a net could lead to a surge in current consumption, such extra power consumption situations can be caught with ease. These low power issues can be caught using a vector independent symbolic simulator without the user having an in-depth understanding of power management modes of operation.


Relentless pursuit of Moore’s law and human ingenuity will continue to bring unforeseen challenges to SoC and interface IP designs. Cutting-edge technologies make it possible to push our design horizons and achieve more complex logic designs. These pursuits will continue to bring bigger challenges in logic verification of custom interface IPs. Symbolic simulation technologies provide unique and powerful solutions to the plethora of technical challenges faced by logic verification engineers of interface IPs.

The Synopsys ESP solution offers high-quality equivalence checking for full-custom designs. ESP provides fast and extensive coverage, enabling users to quickly find bugs and have confidence that the Verilog reference design is functionally identical to other Verilog models or its transistor-level implementation.

To learn more about how ESP can help your SoC and interface IP designs, please visit the Synopsys website.

Leave a Reply

(Note: This name will be displayed publicly)