Transcript Verifying a Specification

Writing, Verifying and Exploiting Formal
Specifications for Hardware Designs
Chapter 3: Verifying a Specification
Presenter: Scott Crosby
The problem
• Specifications have problems
– Incorrect
– Buggy
– No hardware to compare
What they have
•
•
•
•
‘Spell check’ a specification
Check for correctness properties
Automatically generate test sequences
Proof it can be implemented
– With no explicit state machine
Reminders
• Specification:
– No explicit state machine
– Monitor
• Judge
• Deterministic
Mealy Machine
Properties of Properties
• List of properties
– Grouped by the agent
• Correcti = agent i is correct
– ANTECEDENT  CONSEQUENT
• Consequent
– Λ,V,¬, prev()
• Antecedent
– Λ,V,¬, prev()
– prev(trdy Λ stop)  stop
Temporal or Causal
• Cause  Effect
– prev(trdy)  ¬prev(stop) V stop
• Past Conditions  Current State
– prev(trdy Λ stop)  stop
Property Representation
• Restricted linear time
– prev(ANTECEDENT)  CONSEQUENT
• Consequent
– Λ,V,¬, and this agents outputs variables
• Antecedent
– Λ,V,¬, prev(), any agents output variables
Properties of Properties
• Separable
– Only describes outputs of one agent
– Eg, mutual exclusion not explicit
• No nondeterminism
• Implementable
• Correctness only function of own outputs
Correctness of Specifications
• Problems
– Too strict
– Too loose
• What we want
– No implementation
– No state machines
– Avoid state explosion
– Easy to verify
Past Solutions
• Model checking
– Huge state explosion
– What to check?
• Abstract representation
– How abstract?
What this offers
• Checking specifications for correctness
• Generating sample outputs
• Proof of implementability
Checking Specifications
• Specification
– Restricted LTL
• Model checker
– CTL
• Three ‘Spell Checks’
• Human written characteristics
CTL
• Branching time logic
• Logic operators
– Λ,V,¬
• Temporal
– EX, EG, E[a U b]
• Derived
– AX, EF, A[a U b], AF
‘Spell Check’ of a specification
• Dead state
‘Spell Check’ of a specification
• Dead state
address_phase=true
irdy=false
trdy=true
stop=false
‘Spell Check’ of a specification
• Under-restriction
‘Spell Check’ of a specification
• Vacuous property
– Every property is used
Characteristic Check
• Characteristics
– User written properties
– CTL formula
– Human designed
• Requires debugging
– Reusable
Results
• Will see details next friday
• Bugs found in PCI
• Bugs found in Itanium bus protocol
Generator
• Constraint solver
• Traces
Sample output
Generator
• Find missing properties
• Found bug
– Eg, signal must remain constant
– Wasn’t discovered
• Nobody thought to check
Receptiveness Proof
• What is receptiveness?
• Implementability
– Can the spec be implemented?
• Receptiveness
– Can the whole spec be implemented?
– Every choice?
A note
• Spec with dead states is implementable
Property Representation
• Seperability
– prev(ANTECEDENT)  CONSEQUENT
• Consequent
– Λ,V,¬, and this agents outputs variables
• Antecedent
– Λ,V,¬, prev(), any agents output variables
Theorem
• Any specification with
– Separability
– No dead states
• Is receptive
– Whole thing is implementable
– Behaves correctly, regardless of environment
Setup of proof
• Mealy machine
• You vs Environment
You vs Environment
Separability
My choice
No dead states
This Means:
• My correctness doesn’t depend on other’s
behavior at the current time step.
• I always have a choice where I will be
correct.
Corollary 1: Implementability
• If
– No dead states for anyone
– Separability
• Exists a set of machines that implement
the specification.
Corollary 2: Receptiveness
• If
– No dead states for anyone
– Separability
• Exists a set of agent implementations that
will go to every reachable state in system.
Conclusion
• Debug a specification
• Generate a sample run
• Prove that it is implementable