Library

feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Electronic Resource
    Electronic Resource
    Springer
    Formal methods in system design 3 (1993), S. 181-209 
    ISSN: 1572-8102
    Keywords: machine-checked verification ; algorithmic transformation ; retiming ; pipeline ; circuit design
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We show how machine-checked verification can support an approach to circuit design based on two kinds of refinement. This approach starts with a conceptually simple (but inefficient) initial design and uses a combination of ad hoc refinement and algorithmic transformation to produce a design that is more efficient (but more complex). We present an example in which we start with a simplified CPU design and derive an efficient pipelined form, including circuitry for reverting the effects of partially executed instructions when a successful branch is detected late in the pipeline. The algorithmic stage of our derivation applies a transormation, retiming, that has been proven to preserve functional behavior in the general case. The ad hoc stage requires special justification, which we supply in the form of a machine-checked formal verification.
    Type of Medium: Electronic Resource
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 2
    Electronic Resource
    Electronic Resource
    Springer
    Theory of computing systems 17 (1984), S. 13-27 
    ISSN: 1433-0490
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract A super-polynomial lower bound is given for the size of circuits of fixed depth computing the parity function. Introducing the notion of polynomial-size, constant-depth reduction, similar results are shown for the majority, multiplication, and transitive closure functions. Connections are given to the theory of programmable logic arrays and to the relativization of the polynomial-time hierarchy.
    Type of Medium: Electronic Resource
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 3
    Electronic Resource
    Electronic Resource
    Springer
    Algorithmica 6 (1991), S. 5-35 
    ISSN: 1432-0541
    Keywords: Digital circuitry ; Graph theory ; Linear programming ; Network flow ; Optimization ; Pipelining ; Propagation delay ; Retiming ; Synchronous circuitry ; Systolic circuits ; Timing analysis
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics
    Notes: Abstract This paper describes a circuit transformation calledretiming in which registers are added at some points in a circuit and removed from others in such a way that the functional behavior of the circuit as a whole is preserved. We show that retiming can be used to transform a given synchronous circuit into a more efficient circuit under a variety of different cost criteria. We model a circuit as a graph in which the vertex setV is a collection of combinational logic elements and the edge setE is the set of interconnections, each of which may pass through zero or more registers. We give anO(¦V∥E¦lg¦V¦) algorithm for determining an equivalent retimed circuit with the smallest possible clock period. We show that the problem of determining an equivalent retimed circuit with minimum state (total number of registers) is polynomial-time solvable. This result yields a polynomial-time optimal solution to the problem of pipelining combinational circuitry with minimum register cost. We also give a chacterization of optimal retiming based on an efficiently solvable mixed-integer linear-programming problem.
    Type of Medium: Electronic Resource
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 4
    Electronic Resource
    Electronic Resource
    Springer
    Discrete & computational geometry 4 (1989), S. 591-604 
    ISSN: 1432-0444
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics
    Notes: Abstract We present an algorithm for computing certain kinds of three-dimensional convex hulls in linear time. Using this algorithm, we show that the Voronoi diagram ofn sites in the plane can be computed in Θ(n) time when these sites form the vertices of a convex polygon in, say, counterclockwise order. This settles an open problem in computational geometry. Our techniques can also be used to obtain linear-time algorithms for computing the furthest-site Voronoi diagram and the medial axis of a convex polygon and for deleting a site from a general planar Voronoi diagram.
    Type of Medium: Electronic Resource
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...