by Chris Kwok, Priya Viswanathan and Kurt Takara - Mentor, A Siemens Business
Today’s SoC designs integrate many design IP blocks from various providers, each with their own implementation of reset. The reset architecture of a digital design can also be very complex. Designs have multiple sources of reset, such as power-on reset, hardware resets, debug resets, software resets, and watchdog timer reset. Errors in reset design can lead to metastability, glitches or other functional failures of the system. Furthermore, complex interactions can occur with the convergence of multiple resets, multiple clocks and multiple power domains. In many cases, this leads to a reset tree that is larger and more complex than the clock tree. Many of the concerns related to clock tree synthesis and load balancing now apply to the reset tree as well. Clearly, it’s a challenge to ensure that all sources of reset propagate safely to the intended destinations under all conditions!
by Jin Hou - Mentor, A Siemens Business
Formal assertion-based verification uses formal technologies to analyze if a design satisfies a given set of properties. Formal verification doesn’t need simulation testbenches and can start much earlier in the verification process. There are three possible results for an assertion after formal runs: “proven,” “fired,” and “inconclusive.” Proven means that formal has done exhaustive mathematic analysis and proved the design satisfies the assertion and no legal stimulus sequence can violate the assertion. Fired means that formal has found an error trace showing the assertion violation. Inconclusive means that formal has only found bounded proof result, i.e., the assertion is true for the bounded cycle, but may be true or false for longer cycles. An inconclusive result cannot guarantee the design function associated with the assertion is correct.
by Joe Hupcey III and Bryan Ramirez - Mentor, A Siemens Business
The number one priority in vehicle security is to harden the root-of-trust; from which everything else—the hardware, firmware, OS, and application layer’s security—is derived. If the root-of-trust can be compromised, then the whole system is vulnerable. In the near future the root-of-trust will effectively be an encryption key—a digital signature for each vehicle—that will be stored in a secure memory element inside all vehicles.
by Anshul Jain, Verification Engineer, Oski Technology
Most false positives (i.e. missing design bugs) during the practice of model checking on industrial designs can be reduced to the problem of a failing cover. Debugging the root cause of such a failing cover can be a laborious process, when the formal testbench has many constraints. This article describes a solution to minimize the number of model checking runs to isolate a minimal set of constraints necessary for the failure. This helps improve formal verification productivity.
by Ajay Daga, CEO, FishTail Design Automation, and Benoit Nadeau-Dostie, Chief Architect - Mentor, A Siemens Business
Built-In Self-Test (BIST) is widely used to test embedded memories. This is necessary because of the large number of embedded memories in a circuit which could be in the thousands or even tens of thousands. It is impractical to provide access to all these memories and apply a high quality test. The memory BIST (MBIST) tool reads in user RTL, finds memories and clock sources, generates a test plan that the user can customize if needed, generates MBIST IP, timing constraints, simulation test benches and manufacturing test patterns adapted to end-user circuit.
by Jin Zhang, Senior Director of Marketing & GM Asia Pacific, and Vigyan Singhal, President & CEO, OSKI Technology
Planning is key to success in any major endeavor, and the same is true for meaningful formal applications. End-to- End formal, with the goal of achieving formal sign-off, is a task that usually takes weeks if not months to complete, depending on the size and complexity of the design under test (DUT). Dedicating time and effort to planning is of utmost importance. While most formal engineers and their managers understand the need for formal planning, they do not know how to conduct thorough planning to arrive at a solid formal test plan for execution.
by Ram Narayan, Oracle
Project RAPID is a hardware-software co-design initiative in Oracle Labs that uses a heterogeneous hardware architecture combined with architecture-conscious software to improve the energy efficiency of database-processing systems. This article, adapted from a paper we presented at DVCon 2014, describes how formal methods went from being used opportunistically to a central place in the verification methodology of the RAPID SoC. Though not without a learning curve, formal did help the Oracle team achieve its verification goals of finishing on schedule and achieving first pass silicon success.