Browse Prior Art Database

A Method to Optimize Environment Models in Formal Verification

IP.com Disclosure Number: IPCOM000123737D
Original Publication Date: 1999-Apr-01
Included in the Prior Art Database: 2005-Apr-05
Document File: 4 page(s) / 142K

Publishing Venue

IBM

Related People

Baumgartner, J: AUTHOR [+3]

Abstract

Model checking is becoming an increasingly important verification technique because of its ability to exhaustively verify complex designs in an efficient manner. This advantage has made model checking quite popular in the verification of computer designs at the unit level. Almost all computer design companies presently employ model checking to verify the correctness of portions of their designs.

This text was extracted from an ASCII text file.
This is the abbreviated version, containing approximately 41% of the total text.

A Method to Optimize Environment Models in Formal Verification

   Model checking is becoming an increasingly important
verification technique because of its ability to exhaustively verify
complex designs in an efficient manner.  This advantage has made
model checking quite popular in the verification of computer designs
at the unit level.  Almost all computer design companies presently
employ model checking to verify the correctness of portions of their
designs.

   Model checking exhaustively verifies sequential logic by
going through all possible walks (sequences of transitions) of the
logic, and checking that a given design specification is not
violated along the possible walks.  The walks are produced for all
allowed input vector combinations / sequences.  In order to verify
the design under only the valid inputs, an environment (irritator) is
required in combination with the design under test to constrain the
inputs from illegal values.

   A severe limitation of model checking is the state space
explosion problem -- model checking is in general exponential in
computational complexity with respect to the size of the "product
machine" (the cross product of all interacting state machines
comprising the logic being tested).In the current model checking
methodology, the reachable state space and the transition table
include both the state bits of the design as well as those of the
environment.

   This disclosure presents a novel and useful technique that
uses the state bits of the design under test to control the input
behavioral environment.  This invention allows more efficient model
checking due to the overall reduced state space for property
checking, and as a result enables larger designs to be formally
verified.

   The traditional solution to the problem of restricting
inputs for model checking is to define one or more nondeterministic
state machines representing the environment, which stresses the
reactive model under test.  These state machines are often similar to
the (SMV-like) pseudo-code below (the example being a PCI bus master;
assume all signals are active-high).
  variable env_state : {idle, wait_for_grant, frame, data,
  last_data};
  assign initial (env_state) := idle;
    next (env_state) := case
      env_state = idle : {idle,wait_for_grant};
      (env_state = wait_for_grant) & GRANT : frame;
      env_state = frame : {data,last_data};
      (env_state = data) & TRDY: {data,last_data};
      (env_state = last_data) & TRDY: idle;
      else : env_state;
    esac;
  define REQUEST := (env_state = wait_for_grant);
  define IRDY := (env_state = data) º (env_state = last_data);
  define FRAME := (env_state = frame) º (env_state = data);
  GRANT and TRDY are outputs of the model, and inputs to the
  environment.  Multiple items, separated by commas within
  braces "{" and "}", represent nondeterministic choices; the
  model checking engine will explore the results...