Browse Prior Art Database

Architectural Verification of Processors using Symbolic Instruction

IP.com Disclosure Number: IPCOM000112783D
Original Publication Date: 1994-Jun-01
Included in the Prior Art Database: 2005-Mar-27
Document File: 4 page(s) / 134K

Publishing Venue

IBM

Related People

Chandra, AK: AUTHOR [+6]

Abstract

Disclosed is a model for representing instruction level symbolic test case templates and a process for generating probing test cases from these templates to verify processor designs.

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

Architectural Verification of Processors using Symbolic Instruction

      Disclosed is a model for representing instruction level
symbolic test case templates and a process for generating probing
test cases from these templates to verify processor designs.

      Detection of errors in processor designs requires setting up of
complex conditions in the test cases involving data interactions
between instructions and interesting relationships between data and
processor facilities.  The notion of symbolic instruction graphs is
introduced as a model for test case templates that can set up such
complex conditions.

Symbolic instruction graphs can have the following types of nodes:

o   Instruction node: This node explicitly specifies an instruction
    node using its opcode.

o   Oneof node: This node consists of a set of tuples (N, W), where N
    is any type of node and W is a non-negative number indicating the
    relative weight with which to choose this particular node N from
    the set.

o   Sequence node:  This node specifies a sequence of nodes, where
    each member node in the sequence is a copy of a specified node
    (of any allowed type), and the number of nodes in the sequence is
    specified by a range of positive integers

o   Data node:  This node specifies a sequence of bytes of data that
    may or may not correspond to a legal instruction sequence.

o   Graph node:  This node consists of an entire symbolic instruction
    graph.

One of the nodes in the symbolic instruction graph is designated as
the start no for the control flow.  A symbolic instruction graph
consists of the nodes described above connected together by directed
edges which can be of the following types.

o   Next Instruction:  This edge indicates the flow of control due to
    sequential execution.

o   Branch Target:  This edge specifies the flow of control if
    sequential execution is broken by a branching instruction.  In
    general, this edge can be used to represent the flow of control
    resulting from instructions that change the instruction address
    counter.

o   Examples of other architecture dependent edges include an edge to
    indicate the target of the S/390* EXECUTE instruction.  Execution
    of the source node of this edge involves also executing the
    instruction node at the destination of this edge type.  If the

    destination node changes the instruction address counter (e.g.,
    branch) then control is transferred to the new instruction
    address.

      The symbolic instruction graph also allows constraints to be
specified on nodes and some of the important constraints are listed
below.

o   Instructions can be constrained to generate or avoid exceptions.
    Instructions like branches can be constrained further by
    specifying whether or not the branch should be taken.

o   Symbolic register names can be used to specify relatio...