Retiming is an optimization technique for synchronous circuits introduced by Leiserson and Saxe in 1983.Although powerful, retiming is not very widely used because it does not handle in a satisfying way circuits whose registers have load enable, synchronous and asynchronous set/clear inputs.We propose an extension of retiming whose basis is the characterization of registers into register classes.The new approach called multiple-class retiming handles circuits with an arbitrary number of register classes.We present results on a set of industrial FPGA designs showing the effectiveness and efficiency of multiple-class retiming.

Covering problems occur at several steps during logic synthesis including two-level minimization and DAG c o v ering.This paper presents a better lower bound computation algorithm and two new pruning techniques that signi cantly improve the eciency of covering problem solvers.We show that these techniques reduce by u p t o three orders of magnitude the time required to solve c o vering problems exactly.

This paper presents a new 2-level logic minimization procedure. It consists of computing in an implicit way the cyclic core of the Boolean function f to be minimized. This computation is done through original transformations of sets covering problems that take full advantage of the metaproduct based implicit set of products manipulations. The computational cost of this new procedure is independent of the number of minterms of the function f and of its number of prime implicants, which allows us to treat functions for which these numbers are so large that it has never been possible to perform a 2level minimization. This method is, as far as we know, the first one that is able to produce the cyclic cores of all the functions of the MCNC benchmark. 1 Introduction The metaproduct based implicit set of products manipulation techniques introduced in [4] have made possible to compute in an implicit way the sets of prime implicants of Boolean functions for which these sets are much too lar...

A unified framework for the verification of synchronous circuits is presented. Within this framework two verification tasks, verification by actual execution and by simulation, can be automatically performed using algorithms based on the same concepts. The first idea is to manipulate sets of states and sets of transitions instead of individual states and individual transitions. The second idea is to represent these sets by Boolean functions and to replace operations on sets with operations on Boolean functions. A definition is presented of the two problems addressed and then the authors present the verification algorithms. It is shown that these algorithms use the standard set operations in addition to two specific operations called 'Pre' and 'Img'. A brief explanation is presented as to why the basic set operations are very efficiently performed when sets are denoted by the typed decision graphs of their characteristic functions. The Boolean operators 'constrain' and 'restrict', and the function 'expand' that support efficiently the 'Img' and 'Pre' operations are presented. Experimental results are presented and discussed.>

Formal verification of finite state machines (FSM) using symbolic manipulations is addressed. It is shown that the use of symbolic manipulations algorithms for the traversal of a FSM can be sublinear in the number of state and input patterns for some classes of machines. A symbolic manipulation algorithm can be directly used as a method for the transformation of a FSM which preserves the observable behavior. It is also shown that a backward traversal of a FSM can also be performed using symbolic techniques.>

The authors present the original extensions brought to PRIAM to automate both the diagnosis and the rectification of the design errors detected by this tool. PRIAM is an industrial automated formal verifier used to check the functional correctness of digital circuits of up to 20000 transistors. These extensions implement a novel approach to diagnosis based on Boolean equation solving. In particular, no enumeration of the faulty patterns is necessary to find out the incorrect gates in the circuit. The diagnosis system can handle any circuit that can be verified by PRIAM.>