Formal Property Verification

References:

  • Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition.
    • Chapter 20

Intro

  • 1994, Intel spent $500 million to recall the Pentium CPU due to a functional bug that produced erroneous floating-point division results that were off by as much as 61/{1,000,000} [112];
  • Simulation-based logic verification is becoming less and less effective due to the growing complexity of the systems;
    • Large systems are often decomposed into blocks
      • each of these blocks is simulated separately in its own environment;
      • full-chip/system simulation is carried out after block-level simulation is stable;
    • A dramatic increase in the effort invested in simulation-based verification
      • a complete simulation environment, including tests, checkers, coverage monitors, and environment models, is developed and maintained for each block;
      • Half of the total design efforts is devoted to verification;
      • The number of bugs is growing exponentially, and hundreds of billions of simulation cycles are consumed;
    • Only a negligible percentage of all possible executions of the design is actually being tested.
  • Formal property verification
    • major advantage: offers an exhaustive verification technology, which is orders of magnitude more efficient than scalar exhaustive simulation.
    • all possible executions of the design are analyzed;
    • no test inputs are required;
    • main deficiency: its limited capacity compared with simulation.
    • early 2000s, handle modles on the order of 10K memory elements; and 100-500K memory elements with complementary automatic model;
    • nowadays: millions of gates and memory elements;

Example:

Int x;
read (x); if x < 0 then x = ~x; print (x);
  • Verification goal: assume x is a 32-bit integer, verify that every legal input the program prints a nonnegative number;
  • Simulation methods: 2^{32} runs to cover the entire input space

  • Formal approach: a single symbolic simulation

    • INPUT: a set of n Boolean variables representing the input bits;
    • OUTPUT: a Boolean expression that reflects the program computation over the input variables;
    • CHECK: the result Boolean expression is nonnegative.

  • Property: a specification of some aspect of a system’s behavior that is considered necessary, but perhaps not sufficient for correct operation.

    • Example: “A mutually exclusive pair of control signals is never asserted simultaneously”;
    • Example: “a packet router chip connected to the PCI bus always conforms to the rules for correct signaling on the bus”
    • Full functional specifications are rare, because of the difficulty in verifying them.
    • More often, a collection of properties considered to be of crucial importance or difficult to check adequately by simulation.

  • In hardware design, formal property verification is used throughout the design cycle.

formal property verification in hardware design flow

Table 20.1:

  • Five major simultaneous activities (rows)

    • Register-transfer level (RTL)
    • Timing
    • Circuit
    • Layout
    • Postsilicon

  • Early stage: architecture and microarchitecture are designed.

    • formal models of the new idea and protocols are developed and formally verified against a set of requirements;
    • Example: a new cache coherance protocol;
    • Usually carried out by the validation team working closely with the architects;

  • RTL verification: while the RLT is being developed.

    • Property can be:
    • from high-level microarchitectural specifications;
      • e.g., the IEEE specificatino of the arithmetic operations;
    • from the implementation constraints that need to be verified on the RTL;
      • e.g., verifying that all timing paths are within the required range.

  • Constraints consumed by synthesis, static timing analysis, and power analysis are formally verified to be valid.

  • Formal property verifiction products for HW:

    • early 1990s, internal CAD groups from Intel, IBM, Motorola, Siemens, and Bell Labs.
    • late 1990s, early 2000s, startups: @HDL, 0-in, Real Intent, Verplex, Jasper.
    • large EDA companies.

  • During the 5 years or so after 2000, intensive efforts have been directed to finding new and fully automatic ways to apply formal methods to software verification.

    • Simulation is currently the main verificatino tool for software;
    • But the increased frequency of fatal and catastrophic software errors is driving the electronic design community to look for better, more exhaustive verification solution.

  • Formal property verification of software:

    • 2000s, Microsoft, verifying Windows NT drivers;
    • Static Driver Verifier Platform from Microsoft, for device vendors;
    • 2000s, EDA startup, Calypto, C-to-Verilog translation validation.

FM Verification Methods and Technologies

  • Automata-theoretic approach
  • Symbolic model checking
  • Satisfiability analysis
  • Interpolation
  • Symbolic simulation
  • Theorem proving

Formal Property Specification

  • Reactive Systems: systems that interact continuously with their environment, receiving input and produce output.

    • Both the hardware design and embedded software generally fall into this class.
    • In constrast to a computer program, such as a compiler, that receives input once, then executes to termination, producing output once.

  • To specify a reactive system: need the valid input/output sequences, not just the correct function from input to output.

    • Use Temporal Logic

  • Temporal Logic

    • assert the truth of a propersition at certain times relative to the present time.
    • e.g., Fp states that p is true at some time in the future; Gp states that p is true at all times in the future.
    • e.g., “it is never the case that signals grant1 and grant2 are asserted at the same time”
      • –> a safety property (some bad condition never occurs).
    • e.g., “if req1 is asserted now, eventually (at some time in the future) grant1 is asserted”
      • –> a liveness property (some good property must eventually occur).
    • To reason about the liveness: must consider infinite executions of a system – only way to violate the property is the execute indefinitely without the occurance of the good condition.

Model Checking

  • verify temporal properties;
  • provide counterexamples that for properties that are false;
  • fully automated verification of temporal properties is generally referred to as “model checking”, in reference to the first such technique developed by Clarke and Emerson[22];
Automata-Theoretic Approach

Property –> Automaton –>

  • Property: a set of acceptable input/output traces of a system;

  • Finite Automaton: accepts exactly the set of traces accepted by the property[33];

    • automaton is a state graph:
    • edges are labeled with input/output pairs;
    • the language of the automaton: the set of input/output traces being accepted;

    • different languages can be defined by defining different notions of the accepting path;

      • e.g., a set of finite traces: define a legal inital and final states;
      • e.g., an accepting infinite path: define the initial states, and the sets of states that may occur infinitely often on an accepting infinite path;

    • Most algorithms for model checking work by translating the property into a finite automaton;

  • System: also represented by an equivalent automaton.

  • Check: “every trace of the system automaton is a trace of the property automaton”

    • Combining the automaton for the complement of the property with the system automaton to produce a product automaton
    • if the product automaton accepts any traces, then the system does not satisfy the property.
    • If finite traces: Can search the state graph of the product automaton for an accepting path;

  • Tools to search in Finite Traces (Brute force way, “explict state”):

    • COSPAN[34]
    • SPIN[6]
    • Murphi[7]
    • quite effective at verifying software-based protocols, cache coherence protocols, and other systems with relatively small state spaces.

  • Problem: state graphs can be prohibitively large.

    • worse case: the number of states == the number of possible configurations of the registers (or other state-holding elements) in the system.

  • Solution: heuristic methods, avoid explicit construction of the state graph.

    • Symbolic model checking

Symbolic Model Checking

SMC

  • Introduced in late 1980s[35,75], in a tool SMV[36];
  • use logical formula to replace concrete values;

  • transitions of a sequential machine becomes a set of Boolean equations (Figure 20.1)

More

Created Mar 21, 2022 // Last Updated Dec 6, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?