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 Graphics
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.
by Roger Sabbagh, Mentor Graphics
Most things in life are not evenly distributed. Consider for example, the sun and the rain. The city of Portland, Oregon gets much more than its fair share of rainy days per year at 164 on average, while in Yuma, Arizona, 90% of all daylight hours are sunny. Or, how about life as an adolescent? Do you remember how some of us were "blessed" with acne, buck teeth and short sightedness, while others with seemingly perfect skin could spend the money they saved on skin cream, braces and eyeglasses to buy all the trendiest designer clothes? No, things are not always meted out in equal measures.
by Paul B. Egan, Rockwell Automation
Traditionally, connectivity verification at the block level has been completed using dynamic simulation, and typically involves writing directed tests to toggle the top level signals, then debugging why signal values did not transition as expected. For modules with a high number of wires and many modes of operation, the number of required tests quickly becomes unmanageable. We were searching for a better approach. This article will explain how we applied formal analysis at the block level, extended this to full chip and describe how we significantly reduced verification time at both the block and chip level. Just like a block and tackle provides a mechanical advantage, the formal connectivity flow provides a verification advantage.
by Ajay Daga, CEO, FishTail Design Automation Inc.
There are two approaches to the verification of design constraints: formal verification and structural analysis. Structural analysis refers to the type of analysis performed by a static timing tool where timing paths either exist or not based on constant settings and constant propagation. Formal verification, on the other hand, establishes the condition under which a timing path exists based on the propagation requirements for the path. These path propagation requirements are then used to prove or disprove constraint properties based on a formal analysis of the design. Structural analysis is fast because it is simple. Formal verification, however, is more complete and less noisy. Formal verification allows engineers to guarantee that their design is safe from silicon issues that result from an incorrect constraint specification. Structural analysis cannot make this claim because it cannot independently establish the correctness of a variety of design constraints.
by Roger Sabbagh, Mentor Graphics
It's no secret. Silicon development teams are increasingly adopting formal verification to complement their verification flow in key areas. Formal verification statically analyzes a design's behavior with respect to a given set of properties. Traditional formal verification comes in the form of model checking which requires hand-coded properties, along with design constraints. While there certainly are some design groups who continue to be successful with that approach, what are getting more widespread adoption in the industry are the automatic approaches which require much less manual setup. Let's take a look at the top five applications