CSE Technical Reports Sorted by Technical Report Number
| TR Number |
Title |
Authors |
Date |
Pages |
| This report introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), an integrated algorithmic frame-work for SAT that unifies several previously propose search-pruning techniques and facilitates identification of additional ones. GRASP is premised on the inevitability of conflicts during search and it s most distinguishing feature is the augmentation of basic backtracking search with a powerful conflict analysis procedure. Analyzing conflicts to determine their causes enables GRASP to backtrack non-chronologically to earlier levels in the search tree, potentially pruning large portions of the search space. In addition, by ³recording² the causes of conflicts, GRASP can recognize and preempt the occurrence of similar conflicts later on in the search. Finally, straightforward bookkeeping of the causality chains leading up toe conflicts allows GRASP to identify assignments that are necessary for a solution to be found. Experimental results obtained from a large number of benchmarks, including many from the field of test pattern generation, indicate that application of the proposed conflict analysis techniques to SAT algorithms can be extremely effective for a large number of representative classes of SAT instances. |
| With improvements in technology, accurate delay modeling of interconnects is becoming increasingly important. Due to decreasing feature sizes,
the spacing between the signal lines is also decreasing. Consequently,
the switching activities on the neighboring lines can have a significant
impact on the delay of the line of interest, and can no longer be ignored.
Accurate modeling of this phenomenon, which we call the proximity effect,
is the subject of this paper. This is similar to the state-dependency of
logic gate delays, where signal delay can be affected by the switching
activities on the side inputs of a gate. We describe an efficient and
accurate delay computation method using precomputed interconnect moments
that treats the coupled lines as uniform, distributed RC lines and does
not make any lumped approximations. This allows the proposed delay model
to be used in a timing analysis tool operating over both gate and
interconnect domains while accounting for state-dependency.
|
| Gurevich Abstract State Machines (ASMs) provide a sound mathematical basis for the specification and verification of systems. An
application of the ASM methodology to the verification of a pipelined
microprocessor (an ARM2 implementation) is described. Both the
sequential execution model and final pipelined model are formalized
using ASMs. A series of intermediate models are introduced that
gradually expose the complications of pipelining. The first
intermediate model is proven equivalent to the sequential model in the
absence of structural, control, and data hazards. In the following
steps, these simplifying assumptions are lifted one by one, and the
original proof is refined to establish the equivalence of each
intermediate model with the sequential model, leading ultimately to
a full proof of equivalence of the sequential and pipelined models.
|
Technical Reports Page
|
|
