Start date: 18 November 2024
Duration: 4 Days, 9am - 3pm each day
Location: Online course
Certificate: N/A
Cost: Members € 650; Non-members € 975
Course code: N/A
Programme overview
Advanced Formal Verification will equip you to tackle complex verification challenges, by taking full advantage of formal verification on your engineering projects.
Advanced topics such as satisfiability, abstractions (e.g., safe, reduction, and induction), formal synthesis and modeling, non-determinism, advanced constraints, under- and over-constraining, and much more are discussed in depth. While the practical labs are run hands-on using specific formal verification tools, the main focus is on the concepts that are applicable to all of the current commercial formal verification tools.
Practical labs comprise approximately 50% of class time and are based around carefully designed hands-on exercises to reinforce learning. The Advanced Formal Verification exercises are built around the open source RISC-V Picorv32 project, applying formal techniques to it and other peripheral modules.
Learning outcomes
Advanced Formal Verification learning outcomes are as follows:
• Learn how to setup formal reset initialization sequences and pre-load state
• Learn how to break down and solve formal verification problems
• Learn different reduction techniques for improving formal analysis
• Learn how to build a formal verification environment
• Learn advanced SVA syntax and techniques to apply formal to more applications
• Learn the difference between safety and liveness properties and when to use them
• Learn about nondeterminism, how it accelerates formal, and how it helps you solve problems
• Learn how to build a formal scoreboard, perform data-integrity checks, and much more
• Learn the formal abstraction process and implement formal abstractions
• Learn how to write various types of constraints and how to constrain formal for sequences and frames of input data
• Learn how to avoid over- and under- constraining
• Learn what sequential equivalency checking is, how to use it, and its various applications
Who is the course for?
This is the follow-on course to Formal Verification Essentials targeted at individuals who already have a working knowledge of formal technologies and some hands-on experience. It is particularly targeted at engineers and teams who want to move to a subject-matter expert level on formal verification, understanding how to plan, use, and implement formal verification on their real-world projects.
This class assumes a working knowledge of SystemVerilog, SystemVerilog Assertion syntax, and formal verification concepts and tools. We strongly recommend prior attendance of the Formal Verification Essentials course (or equivalent experience) prior to attending this course.
Schedule
How Formal Works
Formal algorithms • Counter-examples • Formal engines • Clocking • Initialization and reset sequences • Formal flow and synthesis • Debugging with Formal
Formal Modeling
Formal synthesis • Safety • Liveness • Embedded assertions • Fairness • Formal testbenches • Helper code
Nondeterminism
Free variables • Design symmetry • Data independence • Symbolic constants • Formal testbenches • Formal scoreboarding
Abstractions and Reductions
Complexity in formal • Reduction and safe reduction techniques • The basic abstraction process • Types of abstract models • Design symmetry and data independence • Example of design abstractions • Safe abstractions
Abstract Modeling
Abstract checker models • Abstraction by induction • Abstraction using state machines • Abstraction using events • Data integrity checking • Abstract checker model examples
Constraining Formal
Underconstraining • Overconstraining • Guidelines • Advanced property writing • Constraint dependencies • Determining the minimal constraint set • Error Injection
More On Constraints
Writing constraints for performance • Large input stimulus generation • Constraint dependencies • Helper constraints • Packet-based protocols
Formal Equivalency
Differences between LEC and SEC • How SEC works • Assume-guarantee process • Automatic and user-defined mappings • Helper assertions and hints • Dealing with SEC inconclusives • Applications for SEC
Trainer Profile
Martin Jones has worked for over 25 years as a design and verification consultant for several European semiconductor companies including Ericsson, Arm, Infineon and Verilab during which time he has seen the development of verification languages and methodologies culminating in SystemVerilog and UVM, in addition to formal techniques.
Martin has worked with Doulos for a number of years and specialises in the delivery of SystemVerilog and UVM related courses.
Email training@midasireland.ie for bookings and queries
