NextOp Software Debuts with Focus on Assertion-Based Verification

Assertion Synthesis in Production Use by Several Customers for Functional Verification

SANTA CLARA, Calif., May 6, 2010 -- NextOp Software, Inc. formally introduced itself today as a functional verification provider focused on delivering Assertion-Based Verification solutions that leverage design and testbench information to uncover bugs, expose coverage holes and increase verification observability. NextOp also announced today its flagship assertion synthesis product BugScope™, after four years of development of key technologies and successful work with several customers.                                                                                                                

“Design complexity has adversely impacted our ability to have confidence that the RTL functional verification process is complete. The current engagement between design teams and verification teams is becoming increasingly inadequate; there is a critical need for tools that instill confidence in both teams that their chip will work as intended,” stated Yunshan Zhu, President and CEO of NextOp. “For four years now, NextOp has been focused on building an assertion-based verification solution resulting in its BugScope assertion synthesis product, which is currently in production use by several customers.”

Current Verification Methodology Limitation:  Lack of Adequate Specifications

Today’s verification methodologies include a combination of directed simulation, constrained random simulation, and formal and semi-formal methods.

• Directed simulation utilizes ‘blackbox’ checkers which test input and output behavior for each feature interaction. This approach is fundamentally not scalable due to the number of complex interactions between features.
• Constrained random simulation utilizes external checkers to define the expected behaviors of the Design under Test (DUT). During simulation, the output of the DUT is compared with the checker, and mismatches are used to identify bugs. The checkers and the DUT are typically developed independently based on the architectural specification. It is difficult to write a checker to exactly match the DUT, and as a result, features and interactions are often skipped by the external checkers, including performance related features, exception and interrupt conditions.
• Formal verification uses mathematical analysis to prove or disprove certain properties for all possible legal input stimuli. Complete verification using formal methods requires that users specify sufficient properties to cover all features of the design.

As design complexity grows, it is imperative that an understanding of the design’s structure and intent be infused into the verification process. Regardless of the speed of the simulator or formal engine, the result of verification is only as good as the specification. Without an adequate specification, the debugging cycle will continue to increase, and design and verification teams will be unable to adequately reduce the risk of chip defects that can cause re-spin costs and schedule overruns.

Importance of Assertion-Based Verification

Assertion-based verification enhances directed and constrained random simulation, formal and emulation verification approaches by driving more effective and targeted verification. An Assertion-based Verification approach utilizes assertions and functional coverage properties, which are logic statements that define the intended behavior of signals in the design. 

• Whitebox assertions specify the behaviors of the internal logic and inject observability into the Register Transfer Level (RTL) code. In contrast, traditional blackbox checkers specify the input and output behaviors of the DUT.
• Assertions ensure the correctness of the implementation logic, and the number of assertions needed to verify the design scales linearly with the complexity of the RTL.
• Whitebox functional coverage properties expose corner case behaviors created by implementation and ensure such behaviors are targeted by simulation test vectors.
• Assertions and functional coverage properties can be reused across all verification platforms, including simulation, formal and emulation, and allow cross checking between different test environments. They also facilitate design reuse.

NextOp’s whitepaper on assertion-based verification can be found at www.nextopsoftware.com/assertion-synthesis-assertion-based-verification-whitepaper.html

NextOp Company Focus

NextOp is focused on assertion-based verification solutions that uncover corner case bugs, expose functional coverage holes, and increase verification observability. NextOp’s solutions fit into existing verification methodologies such as simulation, formal and emulation with sufficient capacity to handle complex SoC designs.

“There have been a number of attempts to improve verification over the last 15 years, but the problem is still unsolved. NextOp technology will make it viable to adopt assertion-based verification, which is a good step toward solving this problem,” said John Sanguinetti, NextOp advisor and Forte Design Systems founder and CTO. “The founders’ experience with both the verification technology and semiconductor chip design experience give them a unique perspective to address this issue.”

Assertion Synthesis Product

In a separate announcement today, NextOp announced its flagship assertion synthesis product, BugScope™, a full-chip assertion synthesis product that leverages design and testbench information to automatically generate assertions and functional coverage properties for progressive and targeted verification of complex designs. BugScope is already in production use by multiple semiconductor companies, including Altera, Entropic and Nvidia. For more information on BugScope, please go to www.nextopsoftware.com/BugScope-assertion-synthesis.html

NextOp Management Team

Dr. Yunshan Zhu is President, CEO and co-founder of NextOp Software, Inc. Prior to NextOp, Dr. Zhu was a member of the Advanced Technology Group at Synopsys. Dr. Zhu also worked as a visiting scientist and a post-doc at Carnegie Mellon University where he co-invented the bounded model checking algorithm. Dr. Zhu did his undergraduate study at University of Science and Technology of China and received his Ph.D. in Computer Science from University of North Carolina at Chapel Hill.

Dr. Yuan Lu is Chief Technology Officer and co-founder of NextOp Software, Inc. Prior to NextOp, Dr. Lu was a Principle Scientist in the Enterprise Switching Group at Broadcom.  Dr. Lu received his BS from Shanghai Jiao Tong University and his Ph.D. in Electrical and Computer Engineering from Carnegie Mellon University.

Members of NextOp's advisory board include:

• Dr. John Sanguinetti, founder and CTO of Forte Design System. He was the founder of Chronologic Simulation in 1991 and was the principal architect of VCS, the Verilog Compiled Simulator. Dr. Sanguinetti received his Ph.D. in Computer and Communication Sciences from University of Michigan.
• Dr. David Overhauser, founder of Simplex Solutions (now Cadence). Dr. Overhauser founded Simplex Solutions in 1995 and helped grow the company to become a public company. Dr. Overhauser has a Ph.D. in Electrical Engineering from the University of Illinois and also has degrees in Math and Computer Science.  
• Dr. Randy Bryant, University Professor of Computer Science, Carnegie Mellon University. Prof. Bryant serves as the Dean of School of Computer Science at CMU. Prof. Bryant is the recipient of the Phil Kaufman Award by Electronic Design Automation Consortium (EDAC) and IEEE Council for Electronic Design Automation for his seminal breakthroughs in the area of formal verification.
• Dr. Edmund Clarke, University Professor of Computer Science, Carnegie Mellon University. Prof. Clarke has received numerous awards, including the 2007 ACM Turing award, for his pioneering work in software and hardware verification. Prof. Clarke is a fellow of the ACM and the IEEE and a member of the National Academy of Engineering.

About NextOp

NextOp Software, Inc. is focused on delivering assertion-based verification solutions that allow design and verification teams to uncover bugs, expose functional coverage holes, and increase verification observability. NextOp’s BugScope assertion synthesis is the first product to automatically generate whitebox assertions and functional coverage properties in SVA, PSL and Verilog formats. BugScope’s properties are used to drive progressive, targeted verification via robust, executable design specifications for existing simulation, formal and emulation flows. The company is headquartered at 2900 Gordon Avenue, Suite 100, Santa Clara, CA 95051. For more information, visit www.nextopsoftware.com or call +1 408-830-9885.