Processor Validation

Both the design complexity and number of bugs are increasing exponentially (so they have a linear relationship to each other)

Overview

• Specification: Capture the design concept using SystemC or HDL at appropriate level of abstraction
  • Design Verification: is this what I want?
• Implementation: Use a synthesis tool to generate lower level of abstraction
  • Implementation Verification: does implementation satisfy the specification?

Techniques

• Simulation
  • Validate the design model using tests
  • Cares about inputs
  • No guarantee of covering functional behaviors and corner cases
  • 
  • Types
    • Interpretive Simulation
      • Line-by-line simulation of the HDL code
    • Compiled Simulation
      • Generate C/C++ equivalent of each line of the HDL code, compile the equivalent code along with simulation kernel.
    • Acceleration
      • Generate equivalent code and distribute among various computation nodes
    • Emulation
      • Use reconfigurable fabric for better performance and enable validation in the presence of OS etc.
• Formal Methods
  • Prove properties or equivalence
  • Don’t rely on inputs
  • Currently used for smaller, critical components
  • Types
    • Theorem Proving
      • Prove a theorem about the system correctness
      • Can solve using combinatorial enumeration and search
      • Usage
        1. Derive rules from specification
        2. State the theorem about the correctness of the implementation
        3. Prove the theorem (using an automated theorem prover)
    • Model checking (aka property checker)
      • Check whether design satisfies a property
      • This is used the most often
      • Increase confidence in the correctness of the model
        • The model satisfied enough system properties
        • Study counterexamples, pinpoint the source of the error, correct the model, and try again
    • Satisfiability (SAT) solving
      • Find a satisfiable assignment
      • SAT solving is fundamental in computer science
        • Given a propositional formula in Conjunctive Normal Form, find if there exists an assignment to boolean variables that makes the formula true
        • NP problem
          • but is still applicable because it can often reduce redundancy
      • Usage
        1. Model the design in CNF
        2. Model the property in CNF
        3. Check the satisfiability of the overall CNF
    • Equivalence checking
      • Check whether two designs are equivalent
      • Often uses SAT solvers
    • Symbolic simulation
      • Simulate the design using symbolic inputs instead of real inputs
      • Halfway between these two categories
• Hybrid
  • Directed tests
    • Uses model checking to generate simulation tests that are more efficient than random tests