Development efforts: Phase I
Module 1: SystemVerilog Overview
• Scope:
This module provides an introduction to the SystemVerilog
language, covering its basic data types, procedural and concurrent
statements, module definition, and instantiation. The scope is to
familiarize students with SystemVerilog as a hardware description
and verification language, highlighting its importance in VLSI
design and verification.
Sub Topics
• Basic data types in SystemVerilog
• Procedural and concurrent statements
• Modules and module instantiation
• Importance of SystemVerilog in VLSI design and verification
Module 2: SystemVerilog Processes and Interfaces
• Scope:
This module delves deeper into SystemVerilog processes,
including always blocks with sensitivity lists and initial blocks. It
also covers fork-join constructs and explores the concept of
interfaces for communication between modules. The scope is to
enable students to use these constructs effectively in VLSI design
and verification.
Subtopics
• Always blocks and sensitivity lists
• Initial blocks
• Fork-join constructs
• Interfaces for communication between modules
Module 3: SystemVerilog Assertions
• Scope:
In this module, students learn about SystemVerilog Assertions
(SVA) and their significance in formal verification. The scope
includes understanding the basics of assertions and differentiating
them from simulation-based testbenches. Students will learn how
to use assertions for design correctness checking.
Subtopics
• introduction to formal verification and SVA
• Using assertions for design correctness checking
• Assertions vs. simulation-based testbenches
Module 4: SVA – Building blocks
• Scope:
This module focuses on the fundamental building blocks of
SystemVerilog Assertions, such as simple properties and operators.
Students will learn how to construct basic assertions and utilize
concurrent assertions effectively for hardware verification.
Subtopics
• Simple properties and operators
• Concurrent assertions
Module 5: SVA – Sequences
• Scope:
Students will explore SVA sequences, which play a crucial role in
formal verification. The scope includes understanding the syntax,
semantics, and composition of sequences, as well as their
application for capturing temporal properties.
Subtopics
• SVA sequence syntax and semantics
• Composition of sequences
• Temporal properties using sequences
Module 6: SVA – Properties and Directives
• Scope:
In this module, students will expand on SVA properties and
directives. The scope includes exploring various types of
properties, including temporal and combinational properties.
Students will learn how to use directives to guide formal tools
efficiently in the verification process.
Subtopics
• Types of properties in SVA
• Writing effective properties
• Using directives to guide formal tools
Module 7: Assertion IP – Case Study
• Scope:
This module presents a case study involving Assertion IP, which
helps students understand how to leverage existing assertion
libraries or pre-built assertion IP to enhance the formal verification
process. The scope includes the benefits of reusable assertion
components in accelerating verification tasks.
Subtopics
• Introduction to Assertion IP
• Reusable assertion components
• Case study demonstrating the use of Assertion IP
Module 8: Mathematical theory behind formal
• Scope:
Introduce the mathematical foundations behind formal verification,
including propositional and first-order logic, model checking, and
symbolic reasoning techniques. Explain how these concepts are
applied in formal verification tools.
Subtopics
• Propositional logic
• First-order logic
• Model checking and symbolic reasoning
Module 9: Auxiliary code and LTL
• Scope:
Cover auxiliary code in SVA and its significance in formal
verification. Discuss how to use LTL (Linear Temporal Logic)
properties and its relationship with SVA for more advanced formal
verification scenarios.
Subtopics
• SVA auxiliary code
• Linear Temporal Logic (LTL) and its relationship with SVA
Module 10: Introduction to formal verification
• Scope:
Provide an overview of formal verification techniques,
highlighting their strengths and limitations. Discuss the differences
between simulation-based verification and formal verification.
Subtopics
• Overview of formal verification techniques
• Differences from simulation-based verification
Module 11: Formal verification apps
• Scope:
Explore various applications of formal verification, such as
property checking, equivalence checking, and deadlock
verification. Discuss how formal verification complements other
verification methodologies.
Subtopics
• Property checking
• Equivalence checking
• Deadlock verification
Module 12: Formal verification constraints
• Scope:
Explain how to specify formal verification constraints effectively.
Cover aspects like design constraints, coverage goals, and analysis
settings to guide formal tools efficiently.
Subtopics
• Specifying formal verification constraints
• Design constraints, coverage goals, and analysis settings
Module 13: Formal verification of an FSM Controller
• Scope:
Present a practical example of verifying a Finite State Machine
(FSM) controller using formal verification techniques.
Demonstrate how to write properties and assertions for FSM
verification.
Subtopics
• Verifying Finite State Machine (FSM) controllers using formal
methods
• Writing properties and assertions for FSM verification
Module 14: Formal verification planning
• Scope:
Discuss the importance of formal verification planning and its role
in achieving verification goals. Address how to define a structured
and efficient formal verification plan.
Subtopics
• Importance of formal verification planning
• Defining a structured formal verification plan
Module 15: FV coverage and signoff with formal
• Scope:
Cover formal verification coverage metrics and their significance
in determining verification completeness. Discuss the process of
achieving formal verification signoff.
Subtopics
• Formal verification coverage metrics
• Achieving formal verification signoff
Module 16: Equivalence checking
• Scope:
Introduce equivalence checking as a key aspect of formal
verification. Explain how to use formal techniques to compare two
designs and determine their functional equivalence.
Subtopics
Formal techniques for comparing two designs for functional
equivalence.
Module 17: Deploying Formal
• Scope:
Address the challenges and best practices for deploying formal
verification in real-world VLSI projects. Discuss how to integrate
formal tools into existing verification flows.
Subtopics
• Challenges and best practices for deploying formal verification
in VLSI projects
• Integrating formal tools into verification flows
Module 18: Formal verification practice
• Scope:
Provide practical guidelines for effectively applying formal
verification in VLSI projects. Cover debugging techniques,
iterative refinement, and common pitfalls to avoid.
Subtopics
• Debugging techniques for formal verification
• Iterative refinement and common pitfalls
Module 19: Handling FV Complexity
• Scope:
Discuss strategies for handling the complexity of formal
verification in large-scale designs. Address scalability issues and
efficient resource management.
Subtopics
• Strategies for managing complexity in formal verification
• Scalability and resource management
Module 20: Abstractions in Formal Verification
• Scope:
Explain the use of abstractions in formal verification to manage
complexity and reduce verification time. Discuss different levels of
abstractions and their trade-offs.
Subtopics
• Using abstractions to manage complexity and reduce verification
time
• Levels of abstractions and trade-offs
Module 21: Initial value abstractions
• Scope:
Cover techniques for dealing with initial values in formal
verification. Discuss the challenges associated with uninitialized
values and how to overcome them.
Subtopics
Techniques for handling initial values in formal verification
Module 22: Verifying Memory controllers
• Scope:
Explore the specific challenges and techniques involved in
verifying memory controllers using formal methods. Cover
memory consistency and other relevant topics.
Subtopics
• Challenges and techniques for verifying memory controllers
using formal methods
Module 23: Clock and Reset Verification
• Scope:
Discuss the formal verification of clock domain crossings, clock
domain synchronization, and reset-related issues. Explain how
formal techniques can help ensure proper behavior.
Subtopics
• Formal verification of clock domain crossings and synchronization
• Verification of reset-related issues
Module 24: Formal verification of interrupt controllers
• Scope:
Explain the formal verification of interrupt controllers and their
interactions with other system components. Cover techniques for
verifying interrupt handling and prioritization.
Subtopics
• Formal verification of interrupt handling and prioritization
Module 25: Formal Tools – VC formal [Synopsys team]
• Scope:
Provide an in-depth exploration of the VC Formal tool by
Synopsys. Cover its features, capabilities, and how to effectively
use it for formal verification tasks.
Subtopics
• In-depth exploration of the VC Formal tool by Synopsys
• Features, capabilities, and effective usage for formal verification
Phase II topics
For Phase I of the course, the Subject Matter Expert (SME) can
consider and suggest any of the following additional topics that they
think are fit for ChipEdge students and align well with the course's
objectives and complexity level:
1. Advanced SystemVerilog Assertions (SVA) Constructs
Scope:
Covering more advanced SystemVerilog Assertions (SVA) constructs
such as sequences with multiple cycles, non-regular expressions, and
hierarchical assertions.
Subtopics:
a. Sequences with Multiple Cycles
b. Non-Regular Expressions
c. Hierarchical Assertions
2. Coverage-Driven Formal Verification
Scope:
Explaining how to use coverage metrics to guide the formal verification
process and achieve comprehensive coverage.
Subtopics:
a. Importance of Coverage-Driven Verification
b. Strategies for Utilizing Coverage Metrics
c. Ensuring Comprehensive Coverage
3. SVA Macros and Reusable Properties
Scope:
Demonstrating the creation and usage of SVA macros to build reusable
properties for efficient verification.
Subtopics:
a. Introduction to SVA Macros
b. Creating Reusable Properties with Macros
c. Benefits of SVA Macro-Based Verification
4. Formal Verification of Complex Pipeline Designs
Scope:
Discussing strategies for verifying complex pipeline designs using
formal methods and managing pipeline hazards.
Subtopics:
a. Challenges in Pipeline Verification
b. Techniques for Formal Verification of Pipelines
c. Handling Pipeline Hazards in Formal Analysis
5. Advanced Equivalence Checking Techniques
Scope:
Exploring advanced techniques for equivalence checking of complex
designs, including incremental and hierarchical equivalence checking.
Subtopics:
a. Introduction to Equivalence Checking
b. Incremental Equivalence Checking
c. Hierarchical Equivalence Checking
6. Formal Verification for Memory Consistency
Scope: Covering techniques to verify memory consistency in
multiprocessor systems using formal methods.
Subtopics:
a. Memory Consistency Models
b. Formal Methods for Memory Consistency Verification
c. Ensuring Memory Consistency in Multiprocessor Systems
7. Formal Verification for Security Standards
Scope:
Exploring the application of formal verification techniques to meet
specific security standards (e.g., Common Criteria, ISO/IEC 15408) for
hardware designs.
Subtopics:
a. Overview of Security Standards
b. Techniques for Formal Verification to Meet Security Standards
c. Security Assurance with Formal Methods
8. Formal Verification in Safety-Critical Designs
Scope: Discussing the use of formal verification in safety-critical
designs, emphasizing the verification of safety properties.
Subtopics:
a. Introduction to Safety-Critical Designs
b. Formal Techniques for Safety Verification
c. Ensuring Safety Compliance with Formal Verification
9. Formal Verification of Hardware Accelerators
Scope:
Covering the verification of hardware accelerators designed for specific
tasks (e.g., AI inference, cryptography) using formal methods.
Subtopics:
a. Introduction to Hardware Accelerators
b. Formal Verification Techniques for Hardware Accelerators
c. Verification of Hardware Accelerators for AI and Cryptography
10. Formal Verification of Complex State Machines
Scope: Exploring techniques to verify complex state machines, such as
protocol state machines and complex control units, using formal
methods.
Subtopics:
a. Verification Challenges for Complex State Machines
b. Formal Methods for State Machine Verification
c. Formal Verification of Protocol State Machines
11. Advanced Abstractions in Formal Verification
Scope: Introducing more advanced abstractions to manage design
complexity, such as transaction-level abstractions and functional
coverage abstractions.
Subtopics:
a. Transaction-Level Abstractions
b. Functional Coverage Abstractions
c. Benefits of Advanced Abstractions in Formal Verification
12. Formal Verification of Data Path Designs
Scope:
Discussing methodologies for verifying data path designs and arithmetic
units using formal methods.
Subtopics:
a. Challenges in Data Path Verification
b. Formal Techniques for Data Path Verification
c. Ensuring Correctness of Data Path Designs
