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