Synthesis Methodology for Built-In At-Speed Testing (2009)
Yinghua Li, Alex Kondratyev, Robert Brayton
We discuss a new synthesis flow, which offers the ability to do easy delay testing almost free in terms of its impact on speed and area as compared to corresponding implementations with standard...
3 Now at Lattice Semiconductor Contents (2008)
Adnan Aziz, Robert Brayton, Stephen Edwards, Sunil Khatri, Yuji Kukimoto, Abelardo Pardo, ...
MVSIS 2.0 Programmer’s Manual (2008)
Donald Chai, Jie-hong Jiang, Yunjian Jiang, Yinghua Li, Alan Mishchenko, Robert Brayton
MVSIS is a logic synthesis system, which enhances traditional binary logic synthesis with capabilities related to multi-value logic. This manual introduces the programming environment of MVSIS 2.0...
Cut-Based Inductive Invariant Computation (2008)
Alan Mishchenko, Robert Brayton
This paper presents a new way of computing inductive invariants in sequential designs. The invariants are useful for strengthening inductive proofs in difficult unbounded model checking instances....
Abstract—Two regular circuit structures based on the programmable logic array (PLA) are proposed. They provide alternatives to the widely used standard-cell structure and have better predictability...
MVSIS Code Generation Manual (2008)
This document describes the code generation feature in the MVSIS v1.1 release, including the design flow from high-level specifications and usage of the commands supported. 2
Abstract Sequential Synthesis UsingS1S � (2008)
Adnan Aziz, Felice Balarin, Robert Brayton, Alberto Sangiovanni-vincentelli, Computer Sciences
We present a mathematical framework for analyzing the synthesis of interacting finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in...
Abstract 1 Simplification of Non-Deterministic Multi-Valued Networks (2008)
Alan Mishchenko, Robert Brayton
We discuss the simplification of non-deterministic MV networks and their internal nodes using internal flexibilities. Given the network structure and its external specification, the flexibility at a...
Fast Minimum-Register Retiming via Binary Maximum-Flow (2008)
Aaron P. Hurst, Alan Mishchenko, Robert Brayton
We present a formulation of retiming to minimize the number of registers in a design by iterating a maximum network flow problem. The retiming returned will be the optimum one which involves the...
MVSIS 2.0 user’s manual (2008)
Donald Chai, Jie-hong Jiang, Yunjian Jiang, Yinghua Li, Alan Mishchenko, Robert Brayton
MVSIS is a program modeled after SIS, but the logic network it works on is such that all variables can be multi-valued, each with its own range. We include all the technology-independent...
Jin S. Zhang, Alan Mishchenko, Robert Brayton, Malgorzata Chrzanowska-jeske
Classical two-variable symmetries play an important role in many EDA applications, ranging from logic synthesis to formal verification. This paper proposes a complete circuit-based method that makes...
Vigyan Singhal, Carl Pixley, Adnan Aziz, Shaz Qadeer, Robert Brayton
We study the problem of optimizing synchronous sequential circuits. There have been previous efforts to optimize such circuits. However, all previous attempts make implicit or explicit assumptions...
Vigyan Singhal, Carl Pixley, Robert Brayton
We study the problem of optimizing synchronous sequential circuits. There have been previous efforts to optimize such circuits. However, all previous attempts make implicit or explicit assumptions...
Jie-hong Jiang, Yunjian Jiang, Yinghua Li, Alan Mishchenko, Subarna Sinha, Tiziano Villa, ...
This users manual describes the essential new features included in the MVSIS v1.1 release. 1
SAT-based logic optimization and resynthesis (2008)
Alan Mishchenko, Robert Brayton, Jie-hong Roland, Jiang Stephen Jang
The paper develops a technology-independent optimization and post-mapping resynthesis for combinational logic networks, with emphasis on scalability and efficient implementation. The proposed...
SAT-based logic optimization and resynthesis (2008)
Alan Mishchenko, Robert Brayton, Jie-hong Roland, Jiang Stephen Jang
The paper develops a technology-independent optimization and post-mapping resynthesis for combinational logic networks, with emphasis on scalability and optimizing power. The proposed resynthesis (a)...
Abstract Combinational and Sequential Mapping with Priority Cuts (2008)
Alan Mishchenko, Sungmin Cho, Satrajit Chatterjee, Robert Brayton
An algorithm for technology mapping of combinational and sequential logic networks is proposed and applied to mapping into K-input lookup-tables (K-LUTs). The new algorithm avoids the hurdle of...
Sequential Rewriting and Synthesis (2008)
Robert Brayton, Alan Mishchenko
Present industrial applications require that logic synthesis should be scalable, which means that the algorithms used should have essentially linear complexity in circuit size. For this, we propose...
Alan Mishchenko, Sungmin Cho, Satrajit Chatterjee, Robert Brayton
The paper presents a new algorithm for FPGA technology mapping into K-input LUTs. The algorithm avoids cut enumeration by incrementally computing and updating one good K-feasible cut at each node of...
Satrajit Chatterjee, Alan Mishchenko, Robert Brayton
Enumeration of bounded size cuts is an important step in several logic synthesis algorithms such as technology mapping and re-writing. The standard algorithm does not scale beyond 6 or 7 inputs...
A Linear Time Algorithm for Optimum Tree Placement ABSTRACT (2008)
Satrajit Chatterjee, Zile Wei, Alan Mishchenko, Robert Brayton
Let N be a point placed directed graph and G be a sub-graph of N. We study the point placement problem of optimally re-placing the nodes in G assuming that the remaining nodes in N are fixed. The...
Fast Boolean Matching for LUT Structures (2008)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
This paper addresses the problem of mapping a completelyspecified Boolean function of 16 or fewer variables, into a network of K-input lookup-tables (K-LUTs) where 3 ≤ K ≤ 6. The proposed...
Minimizing Implementation Costs with End-to-End (2008)
Aaron P. Hurst, Alan Mishchenko, Robert Brayton
Abstract- We introduce end-to-end retiming, a paradigm for efficiently evaluating a varied set of global retiming possibilities. The result is a continuous curve of retiming solutions stretching...
Efficient solution of language equations using partitioned representations (2008)
Alan Mishchenko, Robert Brayton
A class of discrete event synthesis problems can be reduced to solving language equations F • X ⊆ S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs...
On Resolution Proofs for Combinational Equivalence ABSTRACT (2008)
Satrajit Chatterjee, Alan Mishchenko, Robert Brayton, U. C. Berkeley
Modern combinational equivalence checking (CEC) engines are complicated programs which are difficult to verify. In this paper we show how a modern CEC engine can be modified to produce a proof of...
Scalable and Scalably-Verifiable Sequential Synthesis (2008)
Alan Mishchenko, Robert Brayton, Stephen Jang
This paper describes an efficient implementation of an effective sequential synthesis operation that uses induction to detect and merge sequentially-equivalent nodes. State-encoding, scan chains, and...
Generation of a Minimal STG from an Implicit Cover (2007)
Luca Carloni, Tiziano Villa, Timothy Kam, Robert Brayton, Alberto Sangiovanni-vincentelli
This report describes how to produce a state transition table (or state transition graph) of an FSM reduced by using implicit minimization algorithms. The cases of ISFSM's (minimized implicitly...
Minimization of Logic Functions using Essential Signature Sets (2007)
Patrick Mcgeer, Jagesh Sanghavi, Robert Brayton, Alberto Sangiovanni Vincentelli
We present a new algorithm for exact two-level logic optimization. It differs from the classical approach; rather than generating the set of all prime implicants of a function, and then deriving a...
Abstract A Theory of Non-Deterministic Networks (2007)
Alan Mishchenko, Robert Brayton
Both non-determinism and multi-level networks compactly characterize the flexibility allowed in implementing a circuit. A theory for representing and manipulating non-deterministic (ND) networks is...
Lucent Technologies and (2007)
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert Brayton
We present a logical formalism for expressing properties of continuous time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete time Markov...
Scalable sequential verification (2007)
Robert Brayton, Alan Mishchenko
Abstract: In general, sequential verification is PSPACE complete, but for application to present-day industrial designs, it needs to be made scalable, which means essentially linear in circuit size....
Improvements to Technology Mapping for LUT-based FPGAs (2007)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
The paper presents several improvements to state-of-theart in FPGA technology mapping exemplified by a recent advanced technology mapper DAOmap [Chen and Cong, ICCAD `04]. Improved cut enumeration...
Improvements to Technology Mapping for LUT-based FPGAs (2007)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
The paper presents several orthogonal improvements to the state-of-the-art in LUT-based FPGA technology mapping. The improvements target delay and area of technology mapping as well as the runtime...
DAG-aware AIG rewriting: A fresh look at combinational logic synthesis (2006)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
This paper presents a technique for preprocessing combinational logic before technology mapping. The technique is based on the representation of combinational logic using And-Inverter Graphs (AIGs),...
Satrajit Chatterjee, Alan Mishchenko, Robert Brayton
Enumeration of bounded size cuts is an important step in several logic synthesis algorithms such as technology mapping and re-writing. Since the standard algorithm enumerates all cuts, it does not...
Using simulation and satisfiability to compute flexibilities in Boolean networks (2006)
Alan Mishchenko, Jin S. Zhang, Subarna Sinha, Jerry R. Burch, Robert Brayton, Malgorzata Chrzanowska-jeske, ...
Abstract—Simulation and Boolean satisfiability (SAT) checking are common techniques used in logic verification. This paper shows how simulation and satisfiability (S&S) can be tightly...
Integrating logic synthesis, technology mapping, and retiming (2006)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
This paper presents a method that combines logic synthesis, technology mapping, and retiming into a single integrated flow. The proposed integrated method is applicable to both standard cell and FPGA...
Improvements to combinational equivalence checking (2006)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
The paper explores several ways to improve the speed and capacity of combinational equivalence checking based on Boolean satisfiability (SAT). State-of-the-art methods use simulation and BDD/SAT...
Improvements to combinational equivalence checking (2006)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
The paper explores several ways to improve the speed and capacity of combinational equivalence checking based on Boolean satisfiability (SAT). State-of-the-art methods use simulation and BDD/SAT...
Jin S. Zhang, Alan Mishchenko, Robert Brayton, Malgorzata Chrzanowska-jeske
Abstract- Classical two-variable symmetries play an important role in many EDA applications, ranging from logic synthesis to formal verification. This paper proposes a complete circuit-based method...
Integrating logic synthesis, technology mapping, and retiming (2006)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
This paper presents a synthesis method that combines logic synthesis, technology mapping, and retiming into a single integrated flow. The proposed integrated method is applicable to both standard...
Efficient Solution of Language Equations Using Partitioned Representations (2005)
Mishchenko, Alan, Brayton, Robert, Jiang, Roland, Villa, Tiziano, Yevtushenko, Nina
A class of discrete event synthesis problems can be reduced to solving language equations f . X ⊆ S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs...
Efficient Solution of Language Equations Using Partitioned Representations (2005)
Mishchenko, Alan, Brayton, Robert, Jiang, Roland, Villa, Tiziano, Yevtushenko, Nina
A class of discrete event synthesis problems can be reduced to solving language equations f . X ⊆ S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs...
An Integrated Technology Mapping Environment (2005)
Alan Mishchenko Satrajit, Alan Mishchenko, Satrajit Chatterjee, Robert Brayton, Maciej Ciesielski
This paper describes a flexible and efficient environment for technology mapping featuring a common set of algorithms for both standard cells and LUT-based FPGAs. The algorithms and data structures...
A Theory of Non-Deterministic Networks (2005)
Alan Mishchenko And, Alan Mishchenko, Robert Brayton
Both non-determinism and multi-level networks can be used to compactly characterize logic structures as well as all the flexibilities allowed for optimizing them. Synthesis results can be improved by...
Integrating Logic Synthesis, Technology Mapping, and Retiming (2005)
Alan Mishchenko Satrajit, Alan Mishchenko, Satrajit Chatterjee, Jie-hong Jiang, Robert Brayton
This paper discusses a synthesis approach, which combines logic synthesis, technology mapping, and retiming into a single integrated flow. The same combination of methods with minor modifications is...
FRAIGs: A unifying representation for logic synthesis and verification (2005)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton
AND-INV graphs (AIGs) are Boolean networks composed of twoinput AND-gates and inverters. In the known applications, such as equivalence checking and technology mapping, AIGs are used to represent and...
An integrated technology mapping environment (2005)
Alan Mishchenko, Satrajit Chatterjee, Robert Brayton, Maciej Ciesielski
This paper describes a flexible and efficient environment for technology mapping featuring a common set of algorithms for both standard cells and LUT-based FPGAs. The algorithms and data structures...
Synthesizing FSMs according to co-Büchi properties (2005)
Guoqiang Wang, Alan Mishchenko, Robert Brayton, Alberto Sangiovanni-vincentelli
Abstract. Computations are developed for the synthesis of an FSM embedded in a known larger system such that the overall behavior satisfies a co-Büchi specification. The procedures for this are very...
A Theory of Non-Deterministic Networks (2003)
Alan Mishchenko, Robert Brayton
Both non-determinism and multi-level networks compactly characterize the flexibility allowed in implementing a circuit. A theory for representing and manipulating non-deterministic (ND) networks is...
Simplification of Non-Deterministic Multi-Valued Networks (2002)
Alan Mishchenko, Robert Brayton
We discuss the simplification of non-deterministic MV networks and their internal nodes using internal flexibilities. Given the network structure and its external specification, the flexibility at a...
Efficient verification and synthesis using design commonalities (1998)
Gitanjali Swamy, Stephen Edwards, Robert Brayton
In this paper we solve the problem of identifying a "matching " between two logic circuits or "networks ". A matching is a functions that maps each gate or...
Structural symmetry and model checking (1998)
Gurmeet Singh Manku, Ramin Hojati, Robert Brayton
Abstract. A fully automatic framework is presented for identifying symmetries in structural descriptions of digital circuits and CTL * formulas and using them in a model checker. The set of...
Verifying Continuous Time Markov Chains (1996)
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert Brayton
. We present a logical formalism for expressing properties of continuous time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete time Markov...
DIMACS Technical Report 96-15 June, 1996 (1996)
Workshop Summary, Robert Brayton, Allen Emerson, Joan Feigenbaum
The correctness of computer hardware and software is an area of growing theoretical interest and practical importance. It is now widely acknowledged that effective reasoning about program correctness...
Workshop Summary: Computational and Complexity Issues in Automated Verification (1996)
Robert Brayton, A. Emerson, J. Feigenbaum
The correctness of computer hardware and software is an area of growing theoretical interest and practical importance. It is now widely acknowledged that effective reasoning about program correctness...
Sequential Synthesis Using S1S (1995)
Adnan Aziz, Felice Balarin, Robert Brayton, Alberto Sangiovanni-Vincentelli
In this paper we propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this will lead to simple, rigorous, and constructive...
Formal Design Verification of Digital Systems (1993)
Thomas Shiple, Adnan Aziz, Felice Balarin, Szu-Tsung Cheng, Ramin Hojati, Timothy Kam, ...
We address the problem of formally proving properties of digital sequential systems. Specifically, our research is focused on building an integrated framework, called HSIS, for supporting automatic...
ESPRESSO-SIGNATURE: A New Exact Minimizer for Logic Functions (1993)
Patrick Mcgeer, Jagesh Sanghavi, Robert Brayton, Alberto Sangiovanni Vincentelli
We present a new algorithm for exact two-level logic optimization which radically improves the QuineMcCluskey (QM) procedure. The new algorithm derives the covering problem directly and implicitly...
Structural Symmetry and Model Checking
Gurmeet Singh Manku, Ramin Hojati, Robert Brayton
A fully automatic framework is presented for identifying symmetries in structural descriptions of digital circuits and CTL* formulas and using them in a model checker. The set of sub-formulas of a...