Formal Verification Testbenches
Using Patterns for Reusable and Repeatable VLSI Design Quality
- 1st Edition - March 1, 2027
- Latest edition
- Authors: Erik Seligman, M .V. Achutha Kiran Kumar, Anshul Jain
- Language: English
Formal Verification (FV) has become an essential technology in the verification of IP, core, or SOC design. The authors' previous book, “Formal Verification: An Essential Toolk… Read more
Description
Description
Formal Verification (FV) has become an essential technology in the verification of IP, core, or SOC design. The authors' previous book, “Formal Verification: An Essential Toolkit for Modern VLSI Design”, offered the definitive guide to design and validation, with advice to help working engineers integrate these techniques into their work. However, understanding the technology is only the beginning: to really use FV effectively, there are many practical considerations in creating effective testbenches. It’s important to use the right formal tools depending on the preferred design style, project phase, and verification goals. Formal Verification Testbenches: Using Patterns for Reusable and Repeatable VLSI Design Quality is designed to provide that guidance, to assist the transition from initial FV usage to FV being the main workhorse of the validation flow. In addition to describing general principles of FV testbench development that apply to any design style, the book takes a deep dive into real testbenches for specific examples: arbiters, sequence controllers, memory controllers, fsm-heavy control blocks, clock gating designs, and dot-product accumulate blocks. It also highlights new opportunities within the field, for example using AI to plan and execute FV. Formal Verification Testbenches: Using Patterns for Reusable and Repeatable VLSI Design Quality enables a design team to confidently plan and execute a project whose primary validation method will be formal verification.
Key features
Key features
- Explains how to write workable formal verification testbenches
- Considers areas within which formal verification is an option
- Discusses techniques for abstracting formal verification problems to make them more tractable
- Teaches the concepts of Architecture formal, compliance Monitor, Arbitration and FPV tools
- Offers practical Testbenches: arbiters, sequence controllers, inter-related FSMs, memory controller, clock gating, CvsRTL on dot product accumulate design, post silicon bug reproduction
- Examines best practices and pitfalls within FV, and considers the future of the field
- Includes a supplementary website containing downloadable code samples.
Readership
Readership
Validation engineers working on chip/IP/SOC designs at the RTL level; VLSI architects, designers and validators, focusing on RTL (Register Transfer Level) models, higher level Architecture models and C/C++ models
Table of contents
Table of contents
Preface: FV For Every Design
P.1. The Validation Crisis and the need for formal verification
P.2. Who is this book for?
P.3. FV is mainstream
P.3.1. Example of how post silicon debug brought in FPV and arch formal in future generations
P.3.2. Example of FV unit where Arch FV, FPV are used
P.4. Formal in all phases of Design
P.4.1. Arch Formal
P.4.2. RTL exercise
P.4.3. FPV
P.4.4. Datapath Formal Verification in the world of Accelerators
P.4.5. Bug hunting
P.4.6. Integration validation: connectivity, control registers
P.4.7. RTL implementation: formal equivalence
P.4.8. Security Verification
P.4.9. Post-Si bug reproduction
P.4.10. Software Formal for Firmware
P.4.11. Low Power FV
P.4.12. AI for FV – where we will discuss in detail in other chapter
P.5. How to get the most out of this book.
P.5.1. Understand your current toolset: are you able to write and compile small RTL models?
P.5.2. Figure out what FV tools are available at your company, try as you read.
P.5.3. This book is for real users: we hope you try these techniques hands-on!
1. Formal Testbench: Overview
1.1. Getting started
1.1.1. Specifications
1.1.2. FVer to start early interaction with Architect/MicroArchitects
1.1.3. Identify opportunities for early Arch FV
1.1.4. Protocol Formal Verification
1.1.5. Failure Driven Development or Complete implementation
1.2. Importance of uarch Specifications
1.2.1. FV completion is as good as specifications
1.2.2. Suggestions when proper Spec is not available
1.2.3. Taking help from existing DV setup
1.2.4. Discussions with Architects/Designers
1.2.5. Automating DV2FV in contexts
1.3. Introduction to Practical RTL Formal Testbenches
1.3.1. Basic Formal Test bench components
1.3.2. Brief about properties
1.3.2.1. Assumptions
1.3.2.2. Assertions
1.3.2.3. Covers
1.3.3. Abstractions/Support Code in case of CvsRTL
1.3.4. Tcl file
1.3.5. Binding SV to SVA
1.3.6. Sign-off Criteria
1.4. Writing Testbenches for Different Levels of Abstraction Useful!
1.4.1. Identifying DUT
1.4.2. Area-Perimeter tradeoff
1.4.3. GenAI applicability ( while there will be a new chapter, we give hints here)
1.4.4. Choosing the right methodology and abstraction
1.4.5. Choosing the right tool
1.4.6. Choosing when are we calling off the activity
1.4.7. Metrics chosen to call activity done
1.5. Simplifications that make formal verification tractable
1.5.1. Reduce size/scope
1.5.2. Simplify inputs
1.5.3. Bounded proofs
1.5.4. State-matching
1.5.5. Domain knowledge
2. Using Basic GenAI (GenFV)
2.1. Review of LLMs and basic concepts
2.1.1. Fundamentals of ML, AI and LLMs
2.1.2. How can LLMs help FV engineer
2.1.3. Review of papers available till date
2.2. AI reading specifications: FVer Interactions
2.2.1. Querying Specifications
2.2.2. Interacting with Specs: Chain Of Thought queries
2.2.3. Interacting with Specs: Prompt Engineering
2.3. Test Plan Generation
2.3.1. GenAI for TP generation from Specifications
2.3.2. Fine Tuning
2.3.3. Recommended prompts for TP generation
2.3.4. Basic Sanity checks
2.4. Property Generation
2.4.1. Generating properties from specs
2.4.2. Generating properties from Test plans
2.4.3. Sanity check of properties
2.4.4. Macros for better property generation
2.4.5. Using DV waveforms for property generation: FSDB2SVA
2.4.6. Creating binding prompts & related tcl files
2.5. Abstract model generation
2.5.1. Create high level model for defined abstractions
2.5.2. Reference files for better model generation
2.5.3. Prompts
2.5.4. Correctness checks
2.6. Connecting all dots together: Preliminary Testplan and implementation
2.6.1. What works and what needs more work
2.6.2. Ways to enhance
2.6.3. RAG?
2.7. Examples
2.7.1. Take open source spec
2.7.2. Create TP
2.7.3. Create properties
2.7.4. Enhance with macros
2.7.5. Create abstractions
2.7.6. Run FV
2.7.7. Collect coverage
3. Architecture formal
3.1. Architecture formal – introduction
3.1.1. Problems with wrong architectures
3.1.2. Timeline of Arch FV – when to be done
3.1.3. Intel story of protocol verification using TLA/TLC
3.1.4. Ptables : Good head start for Arch FV
3.2. Forms of Arch FV
3.2.1. Protocol Formal
3.2.2. Forward progress checks
3.2.3. SV abstraction methods
3.2.4. Algorithm formal
3.2.5. Touch Theorem proving
3.2.6. Abstraction modelling
3.2.7. ISA modelling
3.2.8. Touch Murphi/Promela and other aspects of Arch FV
3.3. Basics of Protocol and definitions
3.3.1. Problems with Protocols
3.3.2. Why FV needed on protocols
3.3.3. What methods available
3.3.4. What can be achieved and what cannot be?
3.3.5. Connecting these properties down stream
3.3.6. One example
3.4. Abstraction modelling
3.4.1. Example model
3.5. Algorithm Formal
3.5.1. Example model
3.6. Failure Driven Development model
3.6.1. Definitions
3.6.2. Example
3.7. SVA modelling
3.7.1. Example
3.7.2. Pitfalls
3.8. Touch on tools available
3.8.1. Academic tools
3.8.2. Vendor tools
3.9. Pointers for further reading
4. Practical Compliance Monitor: Assertion based VIP
4.1. Compliance Monitor – introduction
4.1.1. The opportunity
4.1.2. Usage Model
4.1.3. Planning CompMons in advance
4.1.4. RTL protocol implementation check through CompMons
4.1.5. ABVIP: Connecting from Arch FV
4.1.6. CompMon: Bridges DV and FV
4.2. CompMon as Self-checker (B2B mode)
4.3. Example of one Protocol
4.3.1. Planning on CompMon
4.3.2. Producer – Consumer model / Master – Slave model
4.3.3. Practical coding on assumpions, properties and covers
4.3.4. SV abstraction methods
4.3.5. Demarcation of modes
4.4. Connecting CompMon as Assumption model
4.5. Connecting CompMon in Checker mode
4.6. Connecting CompMon in DV ( parameterized model )
4.6.1. One example
4.7. Abstraction modelling
4.7.1. Example model
4.7.2. Pitfalls
4.8. Touch on various practical Compons available
4.8.1. Academic tools
4.8.2. Vendor tools
4.9. Pointers for further reading
5. First Practical FPV Testbench: Arbiters
5.1. Different forms of Arbiters
5.2. Basic Test plan & Test Setup
5.3. Design Exploration/Exercise
5.4. Basic common properties of Arbiters
5.5. Specific Constraints
5.6. Covers
5.7. Assertions
5.7.1. Forward progress checks
5.7.2. Liveness properties
5.7.3. Fairness
5.7.4. Performance
5.7.5. Security
5.8. Abstractions needed
5.9. Bug Hunting
5.10. Regression Setup
5.11. Sign-off criteria
5.12. Final set of checks
5.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
5.14. Full Proof: goal of converting entire spec to FPV properties
5.15. Integrating FV TB Mainstream
6. Second Practical FPV Test bench: Sequence Controllers
6.1. Introduction of a sequence controller design
6.2. Basic Test plan
6.3. Design Exploration/Exercise
6.4. Basic common properties
6.5. Specific Constraints
6.6. Covers
6.7. Assertions
6.7.1. Forward progress checks
6.7.2. Liveness properties
6.7.3. Fairness
6.7.4. Performance
6.7.5. Security
6.8. Abstractions needed
6.9. Sign-off criteria
6.10. Bug Hunting
6.11. Regression Setup
6.12. Final set of checks
6.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
6.14. Full Proof: goal of converting entire spec to FPV properties
6.15. Integrating FV TB Mainstream
7. Third Practical FV Testbench: Inter-related FSMs
7.1. Introduction of one Inter dependent FSM design
7.2. Basic Test plan
7.3. Design Exploration/Exercise
7.4. Basic common properties
7.5. Divide and Conquer
7.6. Specific Constraints
7.7. Covers
7.8. Assertions
7.8.1. Forward progress checks
7.8.2. Liveness properties
7.8.3. Fairness
7.8.4. Performance
7.8.5. Security
7.9. Abstractions needed
7.10. Sign-off criteria
7.11. Bug Hunting
7.12. Regression Setup
7.13. Final set of checks
7.14. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
7.15. Full Proof: goal of converting entire spec to FPV properties
7.16. Integrating FV TB Mainstream
8. Fourth Practical FPV TB: Memory Controller
8.1. Introduction to a Memory Controller
8.2. Basic Test plan
8.3. Design Exploration/Exercise
8.4. Basic common properties
8.5. Specific Constraints
8.6. Covers
8.7. Assertions
8.7.1. Forward progress checks
8.7.2. Liveness properties
8.7.3. Fairness
8.7.4. Performance
8.7.5. Security
8.8. Abstractions needed
8.9. Sign-off criteria
8.10. Bug Hunting
8.11. Regression Setup
8.12. Final set of checks
8.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
8.14. Full Proof: goal of converting entire spec to FPV properties
8.15. Integrating FV TB Mainstream
9. Fifth Practical FEV TB: Clock gating Design
9.1. Different Applications of FEV
9.2. Introduction to a clock gating design
9.3. Basic Test plan & Setup
9.4. Design Exploration/Exercise
9.5. Basic common properties
9.6. Specific Constraints
9.7. Covers
9.8. Assertions
9.8.1. Forward progress checks
9.8.2. Liveness properties
9.8.3. Fairness
9.8.4. Performance
9.8.5. Security
9.9. Abstractions needed
9.10. Sign-off criteria
9.11. Bug Hunting
9.12. Regression Setup
9.13. Coverage & Formal Test Bench Analysis
9.14. Final set of checks
9.15. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
9.16. Full Proof: goal of converting entire spec to FPV properties
9.17. Integrating FV TB Mainstream
10. Sixth Practical FV TB: CvsRTL on Dot Product Accumulate Design
10.1. Explanation of DPAS design
10.2. Creating a stand-alone C/C++ model from Performance model
10.2.1. Basic Test plan
10.2.2. Design Exploration/Exercise
10.2.3. Basic common Lemmas
10.2.4. Specific Constraints
10.2.5. Covers
10.2.6. Other Lemmas
10.2.6.1. Data Correctness checks
10.2.6.2. Consistency Checks
10.2.6.3. Completeness checks
10.2.7. Abstractions needed
10.2.8. Case splitting and other forms of convergence
10.2.9. Sign-off criteria
10.2.10. Final set of checks
10.2.11. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
10.2.12. Full Proof: goal of converting entire spec to FPV properties
11. Seventh Practical FV TB: Post Silicon Bug Reproduction
11.1. Challenges of post silicon bug reproduction
11.2. Opportunity for FV to add value
11.3. Basic Test plan
11.4. Design Exploration/Exercise
11.5. Methodology
11.6. Specific Constraints
11.7. Covers
11.8. Assertions
11.9. Abstractions needed
11.10. Verifying the fix
11.11. Sign-off criteria
11.12. Final set of checks
11.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
11.14. Full Proof: goal of converting entire spec to FPV properties
12. Best Practices and Pitfalls
12.1. Common Mistakes in Formal Verification Testbenches
12.2. Best Practices for Successful Verification
12.3. Maintenance and Evolution of Testbenches
13. The Future of Formal Verification*
13.1. Emerging Trends in Formal Verification
13.2. Impact of AI and Machine Learning on Verification
13.3. The Role of Formal Verification in Next-gen Technologies
13.4. Future Directions and Opportunities
14. Conclusion
14.1. Summary of Key Insights
14.2. Final Thoughts on the Importance of Formal Verification Testbenches
14.3. Encouragement for Continuous Learning and Improvement
15. Appendix
P.1. The Validation Crisis and the need for formal verification
P.2. Who is this book for?
P.3. FV is mainstream
P.3.1. Example of how post silicon debug brought in FPV and arch formal in future generations
P.3.2. Example of FV unit where Arch FV, FPV are used
P.4. Formal in all phases of Design
P.4.1. Arch Formal
P.4.2. RTL exercise
P.4.3. FPV
P.4.4. Datapath Formal Verification in the world of Accelerators
P.4.5. Bug hunting
P.4.6. Integration validation: connectivity, control registers
P.4.7. RTL implementation: formal equivalence
P.4.8. Security Verification
P.4.9. Post-Si bug reproduction
P.4.10. Software Formal for Firmware
P.4.11. Low Power FV
P.4.12. AI for FV – where we will discuss in detail in other chapter
P.5. How to get the most out of this book.
P.5.1. Understand your current toolset: are you able to write and compile small RTL models?
P.5.2. Figure out what FV tools are available at your company, try as you read.
P.5.3. This book is for real users: we hope you try these techniques hands-on!
1. Formal Testbench: Overview
1.1. Getting started
1.1.1. Specifications
1.1.2. FVer to start early interaction with Architect/MicroArchitects
1.1.3. Identify opportunities for early Arch FV
1.1.4. Protocol Formal Verification
1.1.5. Failure Driven Development or Complete implementation
1.2. Importance of uarch Specifications
1.2.1. FV completion is as good as specifications
1.2.2. Suggestions when proper Spec is not available
1.2.3. Taking help from existing DV setup
1.2.4. Discussions with Architects/Designers
1.2.5. Automating DV2FV in contexts
1.3. Introduction to Practical RTL Formal Testbenches
1.3.1. Basic Formal Test bench components
1.3.2. Brief about properties
1.3.2.1. Assumptions
1.3.2.2. Assertions
1.3.2.3. Covers
1.3.3. Abstractions/Support Code in case of CvsRTL
1.3.4. Tcl file
1.3.5. Binding SV to SVA
1.3.6. Sign-off Criteria
1.4. Writing Testbenches for Different Levels of Abstraction Useful!
1.4.1. Identifying DUT
1.4.2. Area-Perimeter tradeoff
1.4.3. GenAI applicability ( while there will be a new chapter, we give hints here)
1.4.4. Choosing the right methodology and abstraction
1.4.5. Choosing the right tool
1.4.6. Choosing when are we calling off the activity
1.4.7. Metrics chosen to call activity done
1.5. Simplifications that make formal verification tractable
1.5.1. Reduce size/scope
1.5.2. Simplify inputs
1.5.3. Bounded proofs
1.5.4. State-matching
1.5.5. Domain knowledge
2. Using Basic GenAI (GenFV)
2.1. Review of LLMs and basic concepts
2.1.1. Fundamentals of ML, AI and LLMs
2.1.2. How can LLMs help FV engineer
2.1.3. Review of papers available till date
2.2. AI reading specifications: FVer Interactions
2.2.1. Querying Specifications
2.2.2. Interacting with Specs: Chain Of Thought queries
2.2.3. Interacting with Specs: Prompt Engineering
2.3. Test Plan Generation
2.3.1. GenAI for TP generation from Specifications
2.3.2. Fine Tuning
2.3.3. Recommended prompts for TP generation
2.3.4. Basic Sanity checks
2.4. Property Generation
2.4.1. Generating properties from specs
2.4.2. Generating properties from Test plans
2.4.3. Sanity check of properties
2.4.4. Macros for better property generation
2.4.5. Using DV waveforms for property generation: FSDB2SVA
2.4.6. Creating binding prompts & related tcl files
2.5. Abstract model generation
2.5.1. Create high level model for defined abstractions
2.5.2. Reference files for better model generation
2.5.3. Prompts
2.5.4. Correctness checks
2.6. Connecting all dots together: Preliminary Testplan and implementation
2.6.1. What works and what needs more work
2.6.2. Ways to enhance
2.6.3. RAG?
2.7. Examples
2.7.1. Take open source spec
2.7.2. Create TP
2.7.3. Create properties
2.7.4. Enhance with macros
2.7.5. Create abstractions
2.7.6. Run FV
2.7.7. Collect coverage
3. Architecture formal
3.1. Architecture formal – introduction
3.1.1. Problems with wrong architectures
3.1.2. Timeline of Arch FV – when to be done
3.1.3. Intel story of protocol verification using TLA/TLC
3.1.4. Ptables : Good head start for Arch FV
3.2. Forms of Arch FV
3.2.1. Protocol Formal
3.2.2. Forward progress checks
3.2.3. SV abstraction methods
3.2.4. Algorithm formal
3.2.5. Touch Theorem proving
3.2.6. Abstraction modelling
3.2.7. ISA modelling
3.2.8. Touch Murphi/Promela and other aspects of Arch FV
3.3. Basics of Protocol and definitions
3.3.1. Problems with Protocols
3.3.2. Why FV needed on protocols
3.3.3. What methods available
3.3.4. What can be achieved and what cannot be?
3.3.5. Connecting these properties down stream
3.3.6. One example
3.4. Abstraction modelling
3.4.1. Example model
3.5. Algorithm Formal
3.5.1. Example model
3.6. Failure Driven Development model
3.6.1. Definitions
3.6.2. Example
3.7. SVA modelling
3.7.1. Example
3.7.2. Pitfalls
3.8. Touch on tools available
3.8.1. Academic tools
3.8.2. Vendor tools
3.9. Pointers for further reading
4. Practical Compliance Monitor: Assertion based VIP
4.1. Compliance Monitor – introduction
4.1.1. The opportunity
4.1.2. Usage Model
4.1.3. Planning CompMons in advance
4.1.4. RTL protocol implementation check through CompMons
4.1.5. ABVIP: Connecting from Arch FV
4.1.6. CompMon: Bridges DV and FV
4.2. CompMon as Self-checker (B2B mode)
4.3. Example of one Protocol
4.3.1. Planning on CompMon
4.3.2. Producer – Consumer model / Master – Slave model
4.3.3. Practical coding on assumpions, properties and covers
4.3.4. SV abstraction methods
4.3.5. Demarcation of modes
4.4. Connecting CompMon as Assumption model
4.5. Connecting CompMon in Checker mode
4.6. Connecting CompMon in DV ( parameterized model )
4.6.1. One example
4.7. Abstraction modelling
4.7.1. Example model
4.7.2. Pitfalls
4.8. Touch on various practical Compons available
4.8.1. Academic tools
4.8.2. Vendor tools
4.9. Pointers for further reading
5. First Practical FPV Testbench: Arbiters
5.1. Different forms of Arbiters
5.2. Basic Test plan & Test Setup
5.3. Design Exploration/Exercise
5.4. Basic common properties of Arbiters
5.5. Specific Constraints
5.6. Covers
5.7. Assertions
5.7.1. Forward progress checks
5.7.2. Liveness properties
5.7.3. Fairness
5.7.4. Performance
5.7.5. Security
5.8. Abstractions needed
5.9. Bug Hunting
5.10. Regression Setup
5.11. Sign-off criteria
5.12. Final set of checks
5.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
5.14. Full Proof: goal of converting entire spec to FPV properties
5.15. Integrating FV TB Mainstream
6. Second Practical FPV Test bench: Sequence Controllers
6.1. Introduction of a sequence controller design
6.2. Basic Test plan
6.3. Design Exploration/Exercise
6.4. Basic common properties
6.5. Specific Constraints
6.6. Covers
6.7. Assertions
6.7.1. Forward progress checks
6.7.2. Liveness properties
6.7.3. Fairness
6.7.4. Performance
6.7.5. Security
6.8. Abstractions needed
6.9. Sign-off criteria
6.10. Bug Hunting
6.11. Regression Setup
6.12. Final set of checks
6.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
6.14. Full Proof: goal of converting entire spec to FPV properties
6.15. Integrating FV TB Mainstream
7. Third Practical FV Testbench: Inter-related FSMs
7.1. Introduction of one Inter dependent FSM design
7.2. Basic Test plan
7.3. Design Exploration/Exercise
7.4. Basic common properties
7.5. Divide and Conquer
7.6. Specific Constraints
7.7. Covers
7.8. Assertions
7.8.1. Forward progress checks
7.8.2. Liveness properties
7.8.3. Fairness
7.8.4. Performance
7.8.5. Security
7.9. Abstractions needed
7.10. Sign-off criteria
7.11. Bug Hunting
7.12. Regression Setup
7.13. Final set of checks
7.14. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
7.15. Full Proof: goal of converting entire spec to FPV properties
7.16. Integrating FV TB Mainstream
8. Fourth Practical FPV TB: Memory Controller
8.1. Introduction to a Memory Controller
8.2. Basic Test plan
8.3. Design Exploration/Exercise
8.4. Basic common properties
8.5. Specific Constraints
8.6. Covers
8.7. Assertions
8.7.1. Forward progress checks
8.7.2. Liveness properties
8.7.3. Fairness
8.7.4. Performance
8.7.5. Security
8.8. Abstractions needed
8.9. Sign-off criteria
8.10. Bug Hunting
8.11. Regression Setup
8.12. Final set of checks
8.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
8.14. Full Proof: goal of converting entire spec to FPV properties
8.15. Integrating FV TB Mainstream
9. Fifth Practical FEV TB: Clock gating Design
9.1. Different Applications of FEV
9.2. Introduction to a clock gating design
9.3. Basic Test plan & Setup
9.4. Design Exploration/Exercise
9.5. Basic common properties
9.6. Specific Constraints
9.7. Covers
9.8. Assertions
9.8.1. Forward progress checks
9.8.2. Liveness properties
9.8.3. Fairness
9.8.4. Performance
9.8.5. Security
9.9. Abstractions needed
9.10. Sign-off criteria
9.11. Bug Hunting
9.12. Regression Setup
9.13. Coverage & Formal Test Bench Analysis
9.14. Final set of checks
9.15. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
9.16. Full Proof: goal of converting entire spec to FPV properties
9.17. Integrating FV TB Mainstream
10. Sixth Practical FV TB: CvsRTL on Dot Product Accumulate Design
10.1. Explanation of DPAS design
10.2. Creating a stand-alone C/C++ model from Performance model
10.2.1. Basic Test plan
10.2.2. Design Exploration/Exercise
10.2.3. Basic common Lemmas
10.2.4. Specific Constraints
10.2.5. Covers
10.2.6. Other Lemmas
10.2.6.1. Data Correctness checks
10.2.6.2. Consistency Checks
10.2.6.3. Completeness checks
10.2.7. Abstractions needed
10.2.8. Case splitting and other forms of convergence
10.2.9. Sign-off criteria
10.2.10. Final set of checks
10.2.11. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
10.2.12. Full Proof: goal of converting entire spec to FPV properties
11. Seventh Practical FV TB: Post Silicon Bug Reproduction
11.1. Challenges of post silicon bug reproduction
11.2. Opportunity for FV to add value
11.3. Basic Test plan
11.4. Design Exploration/Exercise
11.5. Methodology
11.6. Specific Constraints
11.7. Covers
11.8. Assertions
11.9. Abstractions needed
11.10. Verifying the fix
11.11. Sign-off criteria
11.12. Final set of checks
11.13. Bug Hunting: FPV as supplement to simulation, use to explore risky corner cases
11.14. Full Proof: goal of converting entire spec to FPV properties
12. Best Practices and Pitfalls
12.1. Common Mistakes in Formal Verification Testbenches
12.2. Best Practices for Successful Verification
12.3. Maintenance and Evolution of Testbenches
13. The Future of Formal Verification*
13.1. Emerging Trends in Formal Verification
13.2. Impact of AI and Machine Learning on Verification
13.3. The Role of Formal Verification in Next-gen Technologies
13.4. Future Directions and Opportunities
14. Conclusion
14.1. Summary of Key Insights
14.2. Final Thoughts on the Importance of Formal Verification Testbenches
14.3. Encouragement for Continuous Learning and Improvement
15. Appendix
Product details
Product details
- Edition: 1
- Latest edition
- Published: March 1, 2027
- Language: English
About the authors
About the authors
ES
Erik Seligman
Erik Seligman is currently a Senior Product Engineering Architect at Cadence Design Systems, where he helps to plan and support the Jasper Formal Verification tool suite. Previously he worked at Intel Corporation in Hillsboro, Oregon for over two decades, in a variety of positions involving software, design, simulation, and formal verification. In his spare time he hosts the “Math Mutation” podcast, and has served as an elected director on the Hillsboro school board.
Affiliations and expertise
Senior Product Engineering Architect, Cadence Design Systems, San Jose, California, USAMK
M .V. Achutha Kiran Kumar
M V Achutha Kiran Kumar is an Intel Fellow in the Design Engineering group at intel and leads the company’s Formal Verification Central Technology Office, one of the largest industrial Formal Verification teams in the world. He has over 19 years experience where he worked in various areas of the chip design cycle which includes RTL design, structural design, circuit design, simulation and various levels of validation including formal verification. He is the co-author of 'Formal Verification - An Essential toolkit for the Hardware Design'.
Affiliations and expertise
Intel Corporation, Bengaluru, Karnataka, IndiaAJ
Anshul Jain
Anshul Jain is the Principal Engineer at Intel’s Formal Verification Central Technology Office, and formerly a Formal Verification consultant at Oski Technologies.
Affiliations and expertise
Intel Corporation, Bengaluru, Karnataka, India