CS代考 Microsoft PowerPoint – HW_Verification_Lecture_4

Microsoft PowerPoint – HW_Verification_Lecture_4

Hardware Verification –

Copyright By PowCoder代写 加微信 powcoder

Autumn term 2022

With acknowledgements to colleagues at Arm

• Testbench timing issues
• Introduction to Object-Oriented Programming features
• Randomisation and principles of constrained random simulation
• More details on writing SVAs

• Introduction to Formal Verification
• What is formal verification?
• How formal verification algorithms work
• Properties

• Assertions
• Cover points

• Constraints
• Assumptions
• Clock and reset definitions

• Proven properties
• Bounded or inconclusive proofs
• Counterexamples for properties that fail or cover points that are not reachable

• JasperGold Demo

• “Formal” – applying automated mathematical techniques to reason about a design

• Static testing (simulation is dynamic)
• No stimulus

• Reason about properties of a design
• Property is a logical statement about the design
• Either true or false

• Can give exhaustive proofs
• Property is always true for all possible cases

• Formal verification is an additional technique to increase confidence in the design
• Complementary to simulation-based approach

What is Formal Verification?

• Underlying theory is essentially “mathematical logic”
• Roots dating back to ancient Greeks
• Boole/De Morgan in 19th Century

• Mathematical representation of design/spec
• Prove that design meets spec

• Application driven by CPU vendors (Intel FDIV bug 1994)

• 1990s – Model Checking was invented

A brief history lesson…

• There are different Formal Verification methodologies
• E.g. Model checking, theorem proving, formal semantics, Hoare logic (software)

• Main methodology in digital design is Model Checking
• Primary technique used by Formal Verification EDA tools

• Wikipedia defines Model Checking as follows:
• “Given a model of a system, exhaustively and automatically check whether this model meets a

given specification”

Model Checking

Model Checking

Assertions

Counterexample

Model Checking Tool

RTL Properties
Model of a System

Specification

Model meets
Specification

Model does

specification

• Engineer writes properties about design
• “signal A is always high when signal B is high” B |-> A

• Formal tool proves/disproves asserted property
• Either gives proof – “yes, signal A is always high when signal B is high”
• or counterexample – “no, here is a case where B is high but A is low”

• No stimulus! Just constraints
• also expressed as properties
• assumed rather than asserted
• “Given that signal C never goes high…”

In practice…

• State space = number of unique states the logic can get into
• E.g. ARMv8-A AArch64 operand state space

• 31 general-purpose 64-bit registers
• 2(64×31) = 21984 = 10597

• Number of seconds since The Big Bang ~= 5×1017

• Number of atoms in the Universe ~= 1080

• How can we hope to cover all this?
• Key strength of Formal is efficient, exhaustive

exploration of state space w.r.t. a given property

State Space

• E.g. We want to check a 64-bit adder exhaustively
• For all possible inputs, does it give the correct answer?
• Simulation of all possible inputs:

• One unique set of inputs per cycle
• 2(64×2) = 2128 = 3.4×1038 unique inputs
• Simulation at ~1MHz
• 3.4×1038 simulation cycles = ~1025 CPU years(?!)
• Remember Universe is “only” ~1.3×1010 years old…

• Formal model checker (SAT): CPU seconds

State Space Example

The Real World

• Do we always get full proofs?
• Reality is (sadly) not so rosy…

• Properties can be undetermined

• But it’s not all or nothing
• We can get bounded proofs (more later)
• Formal is good at finding bugs
• Counterexample trace is shortest possible
• If we’ve run a property for a long time and found

no counterexample this increases confidence

• We can use various techniques to improve the chances of success
• State abstractions, invariants

State Space Exploration
Total state space

Useful/legal state

Formal state space

13 © 2019 Arm Limited

State Space Exploration – Simulation

 Depth-first search
 Very large N

14 © 2019 Arm Limited

State Space Exploration – Formal (exhaustive)

Bounded proof: 12345N
 Breadth-first search
 N can get stuck

Some important caveats:
• Covers state space exhaustively for a given property

• Can only find bugs if property can find them

• Proof tool might get “stuck” at cycle N
• What if there’s a bug at cycle N+1?
• Simulation gets deeper quicker

• Bugs can take a very long time to find
• 48 hours CPU time not unusual for corner cases

• How long to run for when we can’t find a proof?
• Cycle depth? How deep is ‘deep enough’?
• CPU time? How long is ‘long enough’?

State Space Exploration – Formal (exhaustive)

Complementary State Space Exploration

Simulation
• Can miss cases due to non-exhaustive

• All checkers active through every trace

(usually…)
• Only as good at finding bugs as the

checkers you write (can use properties)
• State exploration limited by the

stimulus you write
• Coverage is really hard to do well

 Can miss deep cases due to getting

‘stuck’ with N < bug_depth  Each proof attempt considers only one property (usually…)  Only as good at finding bugs as the properties you write  Explores all state until you write constraints to say not to  Coverage is really hard to do well Advantages and Disadvantages on both sides  Complementary approach • Designer-level embedded properties • E.g. “This signal should go high after this one” etc. • Interface specifications • E.g. “The way these blocks communicate is defined by these properties…” • X-Checks • Checking unknown value propagation • Equivalence checking • Prove that two representations of a design exhibit identical behaviour • Liveness properties • Reasoning about deadlock cases, e.g. “We never get stuck in a certain state” • End-to-end properties • E.g. “This instruction should have these architectural effects” Levels of Formal Interface Specifications Block A Block B Want to run formal on Block A embedded properties… … but there’s loads of logic in Block B  Loads more state space for tool to explore… … so let’s just get rid of Block B and treat it as a black box… … but we still need the interface signals to behave correctly, e.g. a request from Block A still needs to be honoured… Interface Properties block_A_props: block_B_props: Formal verification algorithms • Verification by simulation attempts to cover the execution space • Use coverage to measure how much has been tested • Achieving complete coverage is normally not possible • Formal verification instead builds a data structure that captures the results for all possible sequences of the stimulus • Checking properties against this structure verifies them against all possible • Basic mathematical approaches are BDD (binary decision diagrams) • FV tool can uses laws of Boolean algebra to build a representation of the circuit Model Checking • Given a set of properties and a finite state system, a model checking algorithm can search over possible future states and check whether a property is violated • Create space space BDD for initial state • Variables can hold any state unless constraints given • Using system transitions encoded as BDDs, state space BDD can be expanded to include all possible next states • Repeat until all possible future states added to BDD • Eventually a fixed point is reached where no new states are added to Model Checking – what can go wrong? A. A property violation may be detected • Model checker works backwards to create a specific example of how the bad state can be reached B. BDD models can grow exponentially and so time and/or memory limitations can mean that the process has to be terminated prematurely C. Vacuous proofs due to overconstraining the environment Boolean Satisfiability • SAT is an alternative to BDD • The Satisfiability (SAT) problem is: given a Boolean expression, is there a set of values of the variables that will cause the expression to evaluate to ‘1’? • e.g. specification = !a&&!c || b&c; implementation = !(!a&&c) || a&&!b); • Does (implementation -> specification) evaluate to true for any inputs?

• Can we show that there are values where
!(implementation -> specification)

If not, implementation does satisfy the specification

• NP-complete problem
• But using heuristics – strategies that work for some subset of cases –

formal verification can be a powerful technique

Bounded Model Checking using SAT

• BDD techniques incrementally build a representation of all possible
next states

• Until the data structure contains all possible outcomes
• Then properties can be checked in any of the reachable states

• SAT techniques iteratively build an expression that describes all
possible execution paths from the current state

• Concurrently checks that properties are not violated at each step
• Proceeds until either a counterexample is found or the state space expansion

gets too large
• Exhaustive proof may not be possible so it is common to run with a

maximum bound parameter

Techniques to improve success of FV

• Divide and conquer – solve smaller problems first
• Build up knowledge base using previous successes and failures
• Optimise use of the tool – identify critical problems to solve first
• Use domain-specific knowledge – e.g. CPU verification engineers will

know what works and what doesn’t

Using a Formal Verification Tool

• Use the following to drive the tool:
• Assertions
• Cover properties
• Assumptions

• What are the outputs from the tool?
• Exhaustive proofs
• Bounded proofs
• Counterexamples

Assertions

• An assertion is a statement about your logic that should always be true
• Use SVA syntax
• Assertions can be used in simulation and for Formal Verification

valid_opcode: assert property(
@(posedge clk) disable iff (!nrst)
(opcode inside {ADD,SUB,LDR,STR}))
else $fatal (“Invalid opcode”);

Cover Properties

• You may want to check that some condition in your logic can ever
become true

• If you over-constrain your verification testbench, this could prevent a
logic condition ever becoming true

cover_interesting_value: cover property(
@(posedge clk) disable iff (!rst_n)

done && ab == ‘d35);

Precondition Cover Properties

• JapserGold tool will create a precondition cover property
automatically for some assertions

• This will check that the antecedent (expression on the left-hand side)
can be covered (can be true)

• In this example, the cover property will check that valid and req can
both be asserted on a positive edge of the clock

grant_after_request: assert property(
@(posedge clk) disable iff (!nrst)
(valid && req) |-> ##1 gnt)
else $error (“Grant not asserted after request”);

Assumptions

ahblite_stable assume property (
(HTRANS != IDLE) && !HREADY ##1 $stable (HTRANS)
|-> $stable (HWRITE) &&

$stable (HSEL) )
else $error (“HWRITE and HSEL must stay constant if

transaction in progress”);

• An assumption is a constraint on the possible inputs that can be
applied to your design

• An assumption can help restrict the state space over which the
Formal tool has to search

Clock and reset
• Concurrent assertions are normally evaluated on a clock edge and

disabled during reset
• You can either put the clock and reset statements in each assertion
• Or set the defaults – and then save on typing them in each assertion

grant_after_request: assert property(
@(posedge clk) disable iff (!nrst)
(valid && req) |-> ##1 gnt)

default clocking @(posedge clk); endclocking
default disable iff (!nrst);

grant_after_request: assert property(
(valid && req) |-> ##1 gnt)

Clock and reset definitions

• You need to tell the formal tool what to use for the clock
• And tell it what the reset condition is
• Put these statements in the .tcl command file

reset -expression !(rst_n)

Outputs from Formal Verification

• Proven properties (exhaustive proofs)
• Bounded or inconclusive proofs
• Cover points that are not reachable
• Failed properties

• Counterexamples

• We’ll look at these cases in the demo…

• Formal is a powerful tool when applied well
• Exhaustive proofs (but only as good as your properties!)
• Full exploration of state space

• Provides a complementary approach to dynamic verification
• Good at finding bugs that simulation misses
• Increases confidence

Formal Verification – Summary

Next lecture:

Coverage – Functional Coverage and
Code Coverage

程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com