Verification Futures Conference 2024 UK

In the world of formal verification, abstractions along with design reductions, help reduce the state space and make it easier for formal to converge on its proofs.

In this webinar, Doulos Senior Member Technical Staff - Doug Smith will explore the process of abstraction and safe design reductions, and when to use them. Doug will show practical examples of both (using VC Formal from Synopsys) and discuss how to interpret formal results obtained by using abstractions and reductions.

The content will be useful to anyone who wants to learn to make more effective use of formal.

REGISTER NOW FOR THIS FREE KNOWHOW WEBINAR »

Although a formal verification environment can be quickly created with a few simple properties that immediately start finding design issues, it's not easy to model all design behaviors using SystemVerilog's property syntax. This results in complex or numerous properties, or behaviors, that require more than just SVA.

That is where "helper code" comes to the rescue.

In this webinar for formal verification users, we look at when and where helper code can be used effectively to describe properties, model formal abstractions, constrain formal inputs, and control and aid formal analysis. Our goal is to help you accelerate your formal analysis.

Topics include:

• What is helper code?
• Why SVA isn’t always enough
• How helper code aids property development
• How helper code aids formal analysis

The webinar features code running in Siemens Questa™ Formal Apps - however the principles will be useful to anyone with a working understanding of formal verification.

REGISTER NOW FOR THIS FREE KNOWHOW WEBINAR »

This webinar will explore the most common mistakes users of SystemVerilog make. These mistakes have been identified by observing the lab work of students participating in Doulos training classes. The webinar aims to help you avoid the pitfalls and, in the process, get your designs working faster.

Doulos CTI Brian Jensen, will explore the topics listed below and provide useful tips and resources to help you. Practical examples will be provided using QuestaSim from Siemens-EDA in the online simulation environment EDA Playground. The webinar will include live interactive Q&A participation for attendees with Doulos technical experts.

Topics include:

• Wire vs Variable Assignments
• Static vs Automatic Variables
• Static vs Automatic Tasks
• Assignments in Tasks – Pass-by-Copy
• Assignments in Tasks – Pass-by
• Reference
• Enumerations
• struct and packed struct
• Equality Operators
• Equality between vectors
• SVA Temporal Behavior

REGISTER & VIEW THIS WEBINAR NOW »

Nearly all digital designs have asynchronous behaviors. For example, designs often have asynchronous resets or asynchronous inputs like interrupts or ready signals. Some RTL designs are inherently asynchronous in nature as in the case of power management modules receiving off-chip boot up signals. Asynchronous behaviors also appear in the form of asynchronous handshaking protocols for peripheral devices or in the case of synchronizers between clock domain crossings.

SystemVerilog assertions (SVA) provide a great way of testing and describing design behaviors. However, using SVA to capture asynchronous behavior is not always straightforward due to the scheduling semantics of SystemVerilog. While triggering on an asynchronous event is easy enough, the sampling of the assertion inputs is either dependent on its context as in the case of immediate assertions or synchronous by nature as in the case of concurrent assertions. Often, asynchronous events occur before the design has updated its state, requiring the checking of the RTL to be delayed. Further, the timing of asynchronous events may be hard to predict, making it harder to describe using an assertion.

In this paper, eight common asynchronous scenarios are presented and SVA solutions for checking them. In addition, an alternative approach using a global fast clock is presented as both a portable simulation solution and something that works for both formal verification and emulation. Lastly, incorporating functional coverage into the asynchronous checking is also discussed.

VIEW THIS ARTICLE ON THE DOULOS WEBSITE NOW »

This webinar will introduce you to the Universal Verification Methodology.

The aim is to provide you with a base to start learning the rest of UVM, starting at why you would want to use it and the key components of a UVM test bench. The webinar will provide an overview of the DUT interface and Sequencer-Driver communication.

The webinar will help you to understand:

• the class hierarchy
• simulation phases
• transaction-level communication
• sequences and sequencers
• drivers
• the factory
• the configuration database
• objections

This webinar is run in partnership with Siemens EDA and will feature code examples running in the Questa Advanced Simulator. The aim is to help you go on to learn the rest of UVM or to understand the rationale and working of automatically generated UVM code such as that produced by the Siemens EDA UVM Framework and Doulos' Easier UVM code generators.

REGISTER & VIEW THIS WEBINAR NOW »

Is formal verification ready for general use or do you need a PhD to use it? Larger companies continue to recruit formal PhDs into their verification teams while other less-well-qualified engineers seem reluctant to go beyond simplified formal "apps".

So, what is the truth of the matter? Can non-specialist engineers become productive with formal?

In this webinar Doulos Co-Founder and Technical Fellow, John Aynsley will explore the strengths and weaknesses of formal verification.

Using the VC Formal™ tool from Synopsys® as an example, John will explain exactly what you need to know to use formal effectively without acquiring deep knowledge of how it works under-the-hood.

REGISTER & VIEW THIS WEBINAR NOW »

Formal verification is known to work well in areas like control logic, interface protocols, and so on, but it is often dismissed for use on data paths since capacity becomes a significant issue. In particular, packet based protocols have potentially very large state spaces, which can pose a problem for formal. However, in this paper, a step by step process is presented, showing how to decompose a frame of data into simple formal constraints, modeling code, and assertions, which allows formal to fully explore the entire packet state space.

VIEW THIS TUTORIAL ON THE DOULOS WEBSITE NOW »

An advantage of using formal verification is how quickly a formal environment can be created with a few simple properties that immediately start finding design issues. However, not all design behaviors are easily modeled using SystemVerilog's property syntax, resulting in complex or numerous properties, or behaviors that require more than just SVA. That is where helper code comes to the rescue. Helper code can significantly reduce the complexity of properties as well as be used to constrain formal analysis. Likewise, formal analysis may need to reduce the complexity of the problem and state space, which helper code can also help. So where are some places to use helper code and when?

This article looks at how helper code can be used to simplify our properties, model formal abstractions, constrain formal inputs, and aid formal analysis.

VIEW THIS ARTICLE ON THE DOULOS WEBSITE NOW »