Description

Formal verification has a modern history of over 70 years, and yet it is the least understood technology for practical use. Formal methods are used these days to find bugs and sign-off complex hardware designs with over 1.1 billion gates and yet very few people know the secrets of applying it successfully.

In this course, we provide a rigorous introduction to applied formal verification. The course provides a fairly accessible overview of the exciting field of formal methods without requiring you to have any background in formal methods before. The course takes on several myths about formal verification, demystifies it, and describes the successful rules for formal verification adoption.

This course will provide you with a thorough background in formal methods and will help you decide whether you should train yourself further in the science & art of formal verification further. We provide examples that you can play with to get a feel of formal methods from the point of view of theorem proving, property checking and equivalence checking.

We provide answers to the following questions in this course:

1. What are the System-on-chip verification challenges?

2. Why do we need formal verification?

2. What is formal verification?

3. What are the differences between simulation and formal verification?

4. What flow is used in deploying formal verification on projects?

5. What are the implications for verification management when using formal?

Who should attend?

Graduate students in EE, CS, Mathematics, Physics**

Practising engineering professionals 

Semiconductor design and verification engineers

Architects and managers in semiconductor companies


**Students get 20% discount, please email [email protected] from your university/school email account to get your coupon

Why learn formal?

Watch Intro Video

Prerequisites

Passion to learn formal methods

Some knowledge of digital design 

Verilog/VHDL knowledge would help

What you will learn?

Why use formal verification?

History of formal methods

Foundations of formal methods

Deploying formal agile way

 How to prove theorems in HOL 4?

Abstraction, bug hunting, coverage

 Difference between simulation and formal

 How to prove properties with model checkers?

When to use simulation and when to use formal?

Course Bonus

Lifetime access

Student discounts

Live demos

Hands-on experience

Graded Quiz with a Certificate

Use interactive quizzes to test your knowledge

Complimentary monthly, 1-hour group call with Dr Ashish Darbari 

Downloadable source code can be used to replay the demos for experiential learning

Course Curriculum

Video content: 7+ hours

  • 1

    Meet Your Coach

  • 2

    Course Synopsis

  • 3

    Pre-training survey

    • Please tell us what you expect from this course?
  • 4

    Introduction to SoC verification

    • Outline

    • SoC verification: Trends and Challenges

    • Quiz: Introduction to Soc verification
  • 5

    Motivation for formal methods

    • Outline

      FREE PREVIEW

    • Why do we need formal verification?

    • Quiz: Why do we need formal verification?

    • Finding bugs and proofs using automated property sets

    • Live demo of catching bugs in processors using formal
  • 6

    What is formal verification?

    • Outline

    • History of formal verification

    • Quiz: History of formal verification

    • Foundations of formal methods

    • Quiz: Foundations of formal methods

    • Primer on SystemVerilog Assertions

    • Quiz: Primer on SystemVerilog Assertions

    • Coverage

    • Quiz: Coverage
  • 7

    Theorem proving in action

    • Outline

    • Getting started with theorem proving using HOL 4

    • Getting started with theorem proving

    • Simple proofs on Boolean logic

    • Simple proofs on Boolean Logic

    • Modelling a D-type flip-flop without reset

    • Modelling a D-type flip-flop without reset

    • Composing two D-type flip-flops

      FREE PREVIEW

    • Composing two D-type flip-flops

    • Composing N-copies of DFF

    • Composing N-copies of DFF

    • Modelling a D-type flip-flop with asynchronous reset

    • Modelling a D-type flip-flop with asynchronous reset

    • Modelling a D-type flip-flop with an explicit clock

    • Modelling a D-type flip-flop with an explicit clock

    • Further references on theorem proving
  • 8

    Property checking in action

    • Outline

    • Property checking in action

    • Property checking in action

    • Property checking in action

    • Further references on model checking
  • 9

    Equivalence checking in action

    • Outline

    • Equivalence checking in Action

    • Equivalence checking in action
  • 10

    The ABC of formal verification

    • The ABC of formal verification: Outline

    • The ABC of formal verification: Abstractions, Bug hunting & absence and Coverage

    • Quiz: The ABC of formal verification
  • 11

    Automatic end-to-end formal verification of RISC-V processors

  • 12

    Conclusion

Frequently Asked Questions

  • What happens if I need help?

    Yes, we are here to help. Every month you will get an opportunity to get a 1-hour group Zoom call with our experts. All you have to do is to email your questions in advance to [email protected]. You can also engage with fellow students and us in 'the lounge' accessible for free to everyone who enrols on the course.

  • Can I get a certificate with this course?

    Yes, you can, if you complete the full course and obtain a 70% pass mark in the final exam in the course. Your certificate is visible in your account once you sign in. You can go through the content of the full course without passing the final exam; however, you will not get a certificate.

  • What is the difference between this course and other courses offered by Axiomise?

    This is an introductory course that is offered as an on-demand option. Other courses offered by Axiomise are instructor-led face-to-face courses that go from introductory to advanced. Other multi-day courses from Axiomise span anywhere between 16 to 24 hours of course work including intense lab work, theory and quizzes. They can be taken before or after this course.

  • I cannot hear any sound when the video plays.

    By default most browsers set the audio play to default, you can un-mute the video yourself. It is not something we can control on our end.

  • Are there captions to enhance accessibility?

    Yes, all our course content been designed to keep inclusivity in mind therefore all of the videos have closed captions. You can turn them ON/OFF.

  • If I wanted to learn more, can I get help?

    Yes, as we offer more advanced courses, you can take these from us, and we can offer hands-on consulting alongside it to make your experience even more fruitful.

  • What tools do I need for this course?

    You will need to have access to the HOL 4 theorem prover which is free and open-source. You will also need a property checker. Some options for property checkers are Cadence JasperGold, Siemens EDA's QuestaPropcheck, Synopsys VC Formal, OneSpin Solutions 360 DV-Verify, and Yosys HQ's SymbiYosys. Please connect directly with the EDA vendor to obtain a license of the property checking tool.

  • I'm a student, and cannot afford to buy tools.

    For theorem proving, the tool we used is free and open-source. For property checking, most likely you're enrolled in a university where you may access commercial property checking tools. Please contact the property checking tool vendor directly to find out how to obtain their tool license.

  • I have access to tools from the EDA vendors but I need more help in understanding the features. Can you help?

    Yes, we can. Please contact us for more information. We are a vendor-independent house and we work closely with the EDA vendors so we may be able to direct you in the right direction.