BugScopeTM is 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 assertion synthesis takes an RTL design and testbench and automatically synthesizes the following properties:
- High quality assertions, or logic statements which capture key design constraints and specifications. The assertions offer orthogonal perspective from the RTL implementation. Additionally BugScope's assertions complement their blackbox checkers to catch corner-case bugs and improve verification observability.
- Functional coverage properties which expose holes in the testbench. The coverage properties are functional and are independent of the syntax of the RTL. Design and verification teams can use BugScope coverage properties to identify functional coverage holes and guide their test development.
BugScope enhances existing simulation, formal and emulation verification flows by helping design and verification engineers to:
- Uncover corner-case bugs
- Expose functional coverage holes
- Increase verification observability

BugScope has sufficient capacity to support assertion synthesis for full SoC designs, with run-time performance scaling linearly with respect to design complexity.
BugScope's properties
- Are automatically provided in IEEE standard formats such as SVA, PSL or synthesizable Verilog.
- Use temporal operators to capture sequential behaviors and to identify issues among multiple clock cycles.
- Are automatically optimized for maximum performance, incurring minimal overhead to simulation regression.
Assertion Synthesis Enables Assertion-Based Verification Adoption
As design complexity increases, assertions and coverage properties are well-recognized as an important adjunct to the black-box checkers used in simulation and formal verification flows. However, adoption of assertion-based verification has been slow due to the time-consuming task of manually creating high quality assertions and functional coverage properties to the level needed for thorough identification of design problems. For example, it is generally desirable to have one assertion for every 10 to 100 lines of RTL code, yet it can take hours to create, debug and maintain each assertion. Additionally, the high learning curve for standard assertions languages has been a high barrier to adoption.
By automating the tedious and time-consuming process of generating assertions and coverage properties, NextOp BugScope Assertion Synthesis allows design and verification teams to finally reap the benefits of assertion-based verification in a timely and resource efficient manner, mitigating the risk of project delays and defective silicon.
BugScope Assertion Synthesis: Progressive, Targeted Verification
With existing verification approaches alone, it is difficult for verification engineers to determine whether their designs have been sufficiently tested to be declared functionally correct and ready for implementation in silicon. NextOp's BugScope Assertion synthesis adds a mechanism to measure the progress towards this 'verification confidence' over sequential verification cycles. BugScope is easily incorporated into current digital design and verification flows, according to the following use model, which is repeated until verification sign-off.
- Engineers use their RTL and testbench information as input to BugScope.
- BugScope automatically outputs properties in standard formats including SVA, PSL, or Synthesizable Verilog.
- Engineers can review BugScope's reports to classify the new properties into assertions and coverage properties, and then bind them to 3rd party simulators, emulators and formal verification tools in the existing flow.
The properties BugScope initially generates includes a wide mix of both assertions and coverage properties. The prevalence of new coverage properties provides a measurable indicator that there are numerous holes that the verification runs have not covered. Correspondingly, the assertions provide unique 'white-box' observability into each block's targeted behavior, which if triggered clearly identify design bugs.
As development teams progress through their design and verification iterations, the number of coverage properties produced by BugScope will decrease relative to the number of assertions, until such point that there are almost exclusively assertions with only minor coverage properties. Throughout the iterations, the assertions are bound to the corresponding RTL, making sure that any modification of the RTL does not introduce new bugs. When an assertion is triggered, it pinpoints the location of a bug and therefore reduces debug turnaround time.

Facilitating Future RTL reuse
After the completion of a project, assertions will facilitate future RTL reuse. Because BugScope's assertions clearly describe the design intent for each block, the assertion continues to provide confidence that the design integrity is intact regardless of how that block is used in the design. Effectively, the complete design spec becomes both the RTL and the full complement of assertions; any future incorrect usage of the RTL will be caught by the assertions.
BugScope assertion synthesis is available on Linux platforms. Leading edge semiconductor chip companies such as Altera, Entropic and NVIDIA have validated BugScope and adopted it for production use.