SYSTEMVERILOG ASSERTIONS FOR FORMAL VERIFICATION

SYSTEMVERILOG ASSERTIONS FOR FORMAL VERIFICATION

Dmitry Korchemny, Intel Corp.

HVC2013, November 4, 2013, Haifa

November 4, 2013

HVC2013

2

? Most of the examples used in this tutorial are borrowed from our SVA book

November 4, 2013

HVC2013

3

Agenda

? Introduction ? Formal verification model. LTL properties ? Assertion statements ? Sequences and properties ? Clocks and resets ? Assertion system functions ? Metalanguage and checkers ? Local variables ? Recursive properties ? Efficiency and methodology tips ? Future directions and challenges

November 4, 2013

HVC2013

4

INTRODUCTION

November 4, 2013

HVC2013

5

Hardware Verification Task

SPEC (Spec language)

DUT (RTL)

? Does DUT meet the spec? ? Simulation

? Does DUT meet the spec for given input stimuli?

? Formal Verification (FV)

? Does DUT meet the spec for any legal input stimuli?

................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download