Abstract:
This paper presents a method for the verification of speed-independent
circuits. The main contribution is the reduction of the circuit to a set
of complex gates that makes the verification time complexity depend only
on the number of state signals (C elements, RS flip-flops) of the circuit.
Despite the reduction to complex gates, verification is kept exact. The
specification of the environment only requires to describe the transitions
of the input/output signals of the circuit and is allowed to express
choice and non-determinism. Experimental results obtained from circuits
with more than 500 gates show that the computational cost can be
drastically reduced when using hierarchical verification.
Abstract: This paper presents some basic ideas on how to do technology
mapping for DCVSL structures by using Binary Decision Diagrams.
The initial motivation for this research comes from the need to
efficiently synthesize self-timed computational blocks
for asynchronous circuits. However, the proposed ideas can
be also applied in the synchronous world.
Binary Decision Diagrams are the chosen representation
since, besides logic information, they also carry structural information
that can be directly used to synthesize gates.
First, a brief introduction to self-timed systems is
presented. Next, an new approach to map BDDs into
transistor netlist is sketched. The motivation to
use switch-level synthesis tools and new open research
areas on this field are also presented. Finally the
requirement for new layout synthesis tools is commented.
Abstract: This paper presents a method to synthesize labeled Petri nets from
state-based models. Although state-based models (such as Finite State
Machines) are a powerful formalism to describe the behavior of sequential
systems, they cannot explicitly express the notions of concurrency,
causality and conflict. Petri nets can naturally capture these notions.
The proposed method in based on deriving an Elementary Transition System
(ETS) from a specification model that can be mapped into a state-based
representation. Previous work has shown that for any ETS there exists a
Petri net with minimum transition count (one transition for each label)
with a reachability graph isomorphic to the original Transition System.
This paper presents the first known approach to obtain an ETS from a
non-elementary TS and derive a place-irredundant Petri net. Furthermore,
by imposing constraints on the synthesis method, different classes of Petri
nets can be derived from the same reachability graph (pure, free choice,
unique choice).
This method has been implemented and applied in different frameworks:
Petri net composition, synthesis of Petri nets from TSs
generated by asynchronous circuits, and resynthesis of Petri nets.
The results obtained from the experiments have demonstrated the wide
applicability of the method.
Abstract:
UNRET (unrolling and retiming) is an approach for
resource-constrained loop pipelining that aims at finding a loop schedule
with maximum throughput and minimum register pressure.
This paper proposes an algorithm in two phases. In the first phase,
a schedule with maximum
throughput is found for a given set of resource constraints.
To do this, different unrolling degrees
are explored in decreasing order of throughput.
For each theoretical throughput, both the unrolling degree of
the loop
and the expected initiation interval
of the schedule are analytically computed by
using new and effective methods.
In the second phase, the
number of registers required by the schedule is reduced while maintining the
throughput.
The effectiveness of the proposed approach
is shown by presenting results on well-known benchmarks.
Results show that UNRET may obtain faster schedules than
other approaches, also reducing the register pressure.
Abstract: This paper addresses the following problem:
"Given a fixed throughput, finding a schedule of a loop which
minimizes the required resources".
This problem is called Time-Constrained Loop Pipelining.
Time-Constrained Loop Pipelining is an NP-hard problem.
This paper proposes a methodology
to solve it, called TCLP.
TCLP is based on exploring different
sets of resources, looking for a maximum resource utilization.
The main contributions of this paper are the following:
Abstract: The paper presents a systematic method for synthesizing asynchronous circuits from event-based specifications with conflicts on output signals. It describes a set of semantic-preserving transformations performed at the Petri net level, which introduce auxiliary signal transitions implemented by internally analogue components, Mutual Exclusion (ME) elements. The logic for primary outputs can therefore be realized free from hazards and external meta-stability. The technique draws upon the use of standard logic components and two-input MEs, available in a typical design library.
Abstract: This paper presents UNRET (unrolling and retiming), a new approach for resource-constrained software pipelining.UNRET aims at finding a loop schedule with maximum resource usage. UNRET explores schedules in decreasing order of resource usage. For each theoretical resource usage, both the unrolling degree of the loop (K) and the initiation interval of the schedule (II) are analitically computed by using new and effective methods. Next, the loop is unrolled K times and data dependences are successively retimed in order to find a valid schedule with II cycles. The effectiveness of UNRET has been proven by presenting results on different benchmarks. A comparisoon with modulo scheduling is also provided, showing that UNRET can improve results obtained by modulo scheduling.
Abstract: This paper presents a conservative symbolic model checking methodology for speed-independent circuits. The circuit specification is described by using Petri nets, which is the same formalism that several approaches use for synthesis. The thecnique is based on symbolic BDD-based reachability analisys, modeling both the specification and the gate-level network behavior by means of booleans functions. To reduce the size of the BDDs representing these functions, the circuit is partitioned into subcircuits. The global state is kept as the implicit product of subcircuits states, thus verification being conservative, although much more efficient. The applicability of these techniques has been proved by verifying the correctness and speed-independence of some benmarks.ftp.upc.es
Abstract: This paper presents UNRET (unrolling and retiming), a new approach for resource-constrained loop pipelining. UNRET aims at finding a loop schedule with maximum throughput and minimum register pressure. UNRET is composed of two main phases. In the first phase, a schedule with maximum throughput is found for a given set of resource constraints. To do so, different unrolling degrees are explored in decreasing order of throughput. For each theoretical throughput, both the unrolling degree of the loop and the expected initiation interval of the schedule are analytically computed by using new and effective methods. In the second phase, the number of registers required by the schedule is reduced while maintining the throughput. The effectiveness of UNRET has been proven by presenting results on well known benmarks. The obtained results show that UNRET may obtain faster schedules than other approaches, also reducing the register pressure.
Abstract:This paper presents a symbolic model checking methodology for speed-independent circuit verification. The behavior of the environment is described by using Petri nets. The verification technique is based on symbolic BDD-based reachability analysis, modeling both the specification and the gate-level network behavior by means of boolean functions. We present the isomorphism between sets of markings of a safe Petri net and the boolean algebra of n-variable logic functions. We also describe the transition functions to calculate the markings reachable from a set of markings by using the topological information of the Petri net. The verification scenario of our approach is a closed system composed of a Petri net that represents the environment of a circuit, and a net-list of gates of that circuit. Since a signal shared by the environment and the circuit must switch synchronically in both subsystems, we also define a different transition function for input and output signals.Transition functions and sets of states can be represented by boolean functions, therefore we can use BDD to efficiently represent and manipulate them. The verification procedure consists on checking that the circuit conforms to the environment. In other words, we check that the events generated by the circuit are always accepted by the environment, whereas the circuit accepts any event from the environment. The problem is solved by computing all the reachable states of the closed system, and by proving that no failure states can occur. Finally, we prove the applicability of our methodology by verifying the correcn ess of several speed-independent circuits.
Abstract: This technical report presents a set of sufficient conditions for the gate-level synthesis of speed-independent circuits when constrained to a given class of gate libraries. Existing synthesis techniques are restricted to architectures that use simple AND-gates, and do not exploit the advantages offered by the existence of complex gates in libraries. Using typically available complex gates, such as AO-gates and OA-gates, will increase the speed and reduce the area of the circuits obtained by the existing synthesis tools. These improvements are achieved because of:
Abstract: Current algorithms to force the Consistent State Coding (CSC) property for Signal Transition Graphs (STGs) work on the State Graph and, therefore require exponential time and space. Polynomial algorithms have been only proposed for Marked Graphs. In this paper, a P-time algorithm for Unique State Coding (USC) is presented. Although more restrictive than CSC, it is shown that the USC property can be efficiently guaranteed for large STGs. Several experiments evidence that the obtained results are even better than those generated by exponential-time techniques.
Abstract: Methods for the syntesis of asyncronous circuits form Signal Transition Graphs (STGs) have commonly used the State Graph to solve the two main steps of this process:the state assignment problem and the generation of hazard-free logic. The size of the State Graph can be order O(2^n), where n is the number of signals of the circuit. As synthesis tools for asyncronous system start to mature, the size of the STGs increases and the exponential algorithms that work on the State Graph become obsolete. This paper presents alternative algorithms that work in polynomial time and, therefore, avoid the generation of the SG. With the proposed algorithms, STGs can be synthetised and hazard-free circuits generated in extremly low CPU times. Improvements in 2 or 3 orders of magnitude (from hours to seconds) with respect to existing algorithms are archieved when synthesizing fairly large STGs.
Abstract: RISC processors are those who execute a reduced set of instructions in high speed. Generally this kind of processors are fully pipelined to improve latency. This report shows all the research made in the TRISC project to design a 32-bit general-purpose RISC processor using automatic CAD tools for layout synthesis. First we, describe the processor behavior in terms of a Hardware Definition Language. After that a processor logic simulation was performed to check the correctness of the behavioral description. Secondly we obtained a logic description using a behavioral to logic translator, and finally the processor's layout was built using automatic tools to synthesize combinational and sequential blocks, routers, macro cells floorplaners and layout spacers. At the end, some statistical results are shown.
Abstract: Asynchronous systems are gaining acceptance as the size and complexity of digital circuits increase. Concordantly, synthesis tools for asynchronous systems must be developed to make design process easier. This paper aims at the definition of basic concepts for scheduling algorithms in high-level synthesis of asynchronous circuits. New data structures for the representation of events and primitives to manage them are proposed. Two scheduling strategies are also presented and evaluated. Experiments on different benchmarks show that efficient asynchronous schedules can be obtained.