Browse Prior Art Database

A Graphical Interface for Formulating CTL Rules for Model Checking

IP.com Disclosure Number: IPCOM000123197D
Original Publication Date: 1998-Jun-01
Included in the Prior Art Database: 2005-Apr-04
Document File: 3 page(s) / 100K

Publishing Venue

IBM

Related People

Pita, A: AUTHOR [+4]

Abstract

Formal verification using the model checking approach is becoming an established approach in the industry to ensure correctness of the designs. Such verification is best performed at the individual designer level so that logic blocks partitioned at the this level can be exhaustively verified for concurrence with the design specifications. However, in general most logic designers are not familiar with Linear Temporal logic languages, such as CTL (Computational Tree Logic), which are commonly used for specifying the properties to be verified. We describe an intuitive interface that has been developed to formulate rules for model checking.

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

A Graphical Interface for Formulating CTL Rules for Model Checking

   Formal verification using the model checking approach is
becoming an established approach in the industry to ensure
correctness of the designs.  Such verification is best performed at
the individual designer level so that logic blocks partitioned at the
this level can be exhaustively verified for concurrence with the
design specifications.  However, in general most logic designers are
not familiar with Linear Temporal logic languages, such as CTL
(Computational Tree Logic), which are commonly used for specifying
the properties to be verified.  We describe an intuitive interface
that has been developed to formulate rules for model checking.  The
interface allows events to be described in a tree form, similar to a
waveform representation that logic designers are more familiar with
and can use without learning in detail the syntax of languages like
CTL.

   The rules formulated using the interface described here
are in terms of waveforms; values present on model signals at
instances of time.
  For example, given signals X,Y,and Z, the user can construct
   a rule such as:
    (X = 0 & Y = 0)
  which must be followed, between 1 and 3 cycles later, by:
    (Y = 1 & Z = 1).

   This rule is merely a waveform of two events--one
indicating (X = 0 & Y = 0); the other indicating (Y = 1 & Z = 1)
between 1 and 3 cycles after the first.
  Signal    E0 ->E1
          :    :    :
  X             ****
          ----+
          :    :    :
               +----
  Y            |
           ----+
          :    :    :
               +----
  Z        ****
          :    :    :
  where E0 and E1 represent two events, which must happen in the same
sequence as indicated by the waveforms (i.e., E1 after E0).  However,
in order to account for the fact that the desired specification is
"E1 must happen between 1 and 3 cycles after E0", we support the
notion of "min and max delay" between two graphically consecutive
events.  In this case, min_delay = 1 and max_delay = 3.

   Note also that "****" means "don't care" for the
corresponding signal in the corresponding event.

   In this example, the default event connective "->", or
"implies", is used between E0 and E1.  Other connectives are
selectable, such as "and", "finally", or "until", which will be
discussed later.

   The corresponding set of rules for the above waveform
in CTL would be
  AG ( (X=0 & Y=0) -> AX( (Y=1 & Z=1) | AX( (Y=1 & Z=1) |
      AX(Y=1 & Z=1))))

   These type of queries are unambiguous--the user explicitly
defined a rule based upon exact signal values during a timing
window.  However, assume that the model under test has a bug; there
exists a scenario such that E1 cannot happen after E0 with proper
timing.  The above rule will catch this bug.  This re...