log inhelp

Get your own free workspace
View
 

FrontPage

Page history last edited by Erik Seligman 2 years, 10 months ago

Formal Verification:  An Essential Toolkit For Modern VLSI Designers

(class CS-5/610 at Portland State University, Winter Quarter 2009.)

 

What is this class?

Formal Verification (FV) is a powerful technique that enables a designer to directly analyze and mathematically prove the quality of a design, providing 100% coverage of large subsets of the design space without needing to create simulation vectors.  Many modern designers see FV techniques as exotic or academic, though, so their full potential is often not realized in industry design processes.  In this class, we will see that FV has matured significantly, and learn how to apply current leading-edge FV technologies to real VLSI designs using state-of-the-art commercial tools from Cadence and Jasper. 

 

The instructor, Erik Seligman, is a Formal Verification Architect in the Corporate Design Solutions team at Intel, where he has been working since 1994.  This is an engineering class, not a theory class, and will be directly based on techniques he has helped apply to real product designs.

 

Logistics

M/W 1400-1520, Room FAB 150.

 

Standard Disclaimer:  This page represents the opinions of Erik Seligman only, not those of Intel, Portland State University, or any other entity.

Prerequisites

You should have taken at least one class in Digital VLSI Design, or have equivalent work experience, before taking this class.

 

 

Syllabus

 

  1. (Mon 1/5/09) Intro: FDIV & history of FV, FV vs DV, Design flows, types of Formal:  FEV, FPV, CDC, TOV
  2. (Wed 1/7/09) Logic & Foundations: Boolean algebra, identities, implication, LTL, BDDs & SAT
  3. (Mon 1/12/09) Digital RTL design review: Verilog basics, transitors, gates, latches/flops, clocked elements, basic timing issues 
  4. (Wed 1/14/09) Formal Equivalence Verification (FEV) I: FEV basics, comparing designs, mapping state points, proving equivalence, assumptions and constraints
  5. (Wed 1/21/09) FEV II: FEV & schematics: Various exceptions to state-matching
  6. (Mon 1/26/09) FEV III: FEV and complexity: split-casing, cut points, hierarchical partitioning, false negatives, etc.
  7. (Wed 1/28/09) FEV IV: "FEV's Greatest Bloopers": When FEV gives wrong results
  8. (Mon 2/2/09) Assertions: SVA basics, creating assertions in a design, useful assertions, assertions and assumptions, cover points
  9. (Wed 2/4/09) Formal Property Verification (FPV) I: Running the tools, proving your assertions, debugging counterexamples
  10. (Mon 2/9/09) FPV II: Classics of FPV: Examples of good property creation and debug
  11. (Wed 2/11/09) FPV III: FPV as a Design Exploration Tool
  12. (Mon 2/16/09) FPV IV: Cut Points On Steroids:  FPV and complexity issues
  13. (Wed 2/18/09) FPV V: Cool FPV Tricks:  Semi-Formal / Dynamic Formal / Quasi- Formal methods 
  14. (Mon 2/23/09) Guest lecture: Jin Yang (Intel), Symbolic Trajectory Evaluation (STE)
  15. (Wed 2/25/09) Guest lecture: Jesse Bingham (Intel), Connecting High Level Models & RTL
  16. (Mon 3/2/09) SVA 2009: Increased power in assertion creation
    • http://fvclasspsu2009q1.pbwiki.com/f/FV-Lecture16.pptx
    • New assignment:  see ~eseligma/week9_problems.  Note that it may not make much sense until I cover the CDC topic in Wednesday's lecture!
    • Also see below for the final project:  you may begin this as well if you wish.
  17. (Wed 3/4/09) Clock Domain Crossing (CDC) : Metastability and CDC checks
  18. (Mon 3/9/09) Timing Override Verification (TOV): False Paths, Multicycle Paths, and Assertions
  19. (Wed 3/11/09) Putting It All Together:  Guidelines for using FV techniques in real life

 

Final Project:  Due at Noon on Wed 3/18/09

  • Locate a nontrivial (50+-line) design you have created for another class.  You can get one from a classmate or textbook if you don’t have it, or you can just create one from scratch if you want.   The one restriction:  No traffic light controllers allowed.  (I’m sick of those things! )   I have no objection if it is in another language besides Verilog, though you are on your own for any tool-related challenges that result.  (I think both Jasper and Conformal accept VHDL, but you should doible-check on your model.)
  • Use techniques and tools from this class (Jasper, Conformal) to prove or disprove at least 10 aspects of your design.  Each of the 10 may be:

o        A logic-preserving change to your design, that you then verify by comparing two design versions in Conformal.  If you implement 2 or more design changes, include at least one that passes and one that fails FEV.

o        An assertion you create, and then run in Jasper to prove or disprove.  If you implement 2 or more assertions, include at least one that passes and one that fails.

o    An asynchronous clock domain crossing that you check with Conformal.

    

  • Turn in your RTL code, descriptions of your changes or assertions, and tool logs and/or screenshots, in an email to myself &  Fei by noon on Wed 3/18/09. 

 

 

 

 

 

 

Comments (0)

You don't have permission to comment on this page.

PDF version