Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

Global Insertion and Iterative Refinement of Breakpoints in Logic Synthesis Verification

IP.com Disclosure Number: IPCOM000102385D
Original Publication Date: 1990-Nov-01
Included in the Prior Art Database: 2005-Mar-17
Document File: 4 page(s) / 211K

Publishing Venue

IBM

Related People

Clayton, DW: AUTHOR

Abstract

Logic synthesis may be used to translate a netlist representation of a logic design into an alternative netlist representation, e.g., from technology-independent to technology-dependent. One way to verify the correctness of this translation is to compare the original netlist ('model 1') with the new netlist ('model 2') to ensure that they are logically equivalent. A compare program may be written to perform this boolean comparison.

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

Global Insertion and Iterative Refinement of Breakpoints in Logic Synthesis Verification

       Logic synthesis may be used to translate a netlist
representation of a logic design into an alternative netlist
representation, e.g., from technology-independent to
technology-dependent.  One way to verify the correctness of this
translation is to compare the original netlist ('model 1') with the
new netlist ('model 2') to ensure that they are logically equivalent.
A compare program may be written to perform this boolean comparison.

      The compare program may operate by decomposing each model into
segments of combinational logic.  A segment consists of a single net
- either a latch output or a primary output - and all the logic that
feeds it, stopping at other latch outputs or primary inputs.
Provided that nets have signal names such that all points across both
models having the same name are logically equivalent, the compare
program may associate each model 1 segment with its corresponding
model 2 segment by matching signal names.  The program may similarly
match each input of the model 1 segment with each input of the model
2 segment.  This process is called segmentation.

      Considering each pair of matched segments in turn, the program
may compare the two segments by simulating logic patterns on their
inputs and verifying that each gives the same output value in every
case.  Verification is complete when all segment pairs have been
considered.

      A segment in a typical large design may have many hundreds of
inputs and contain several thousand gates.  The processing time
required to simulate all possible logic patterns on the inputs to
this segment will typically exceed 5 minutes.  The design need have
only 100 such segments for the total processing time to become
unreasonable.  This is referred to as the 'large segment problem'.

      One approach to the large segment problem is to insert
'breakpoints' in each model prior to segmentation.  The compare
program may treat breakpoints as it does primary inputs, primary
outputs and latch outputs, and use them in defining the segments.
Thus, a large segment may be broken down into two smaller segments by
inserting a breakpoint somewhere within it.  Processing time is
approximately related to the square of the number of inputs to the
segment, so if the inputs can be halved by adding a breakpoint, then
the total processing time is halved (there are now two segments to
consider).

      Breakpoints may be inserted manually by examination of the
model 1 and 2 netlists.  Candidate points are nets that have the same
signal name in both models.  Manual insertion is labor-intensive,
requires expert knowledge of the design and typically does not
provide an effective set of breakpoints.  A program may be written to
analyze the structure of the design to determine suitable
breakpoints, but this typically requires a complex algorithm and long
processing time, an...