Yunjian Jiang, Slobodan Matic, Robert K. Brayton
Logic evaluation of a Boolean function or relation is traditionally done by simulating its gate-level implementation, or creating a branching program using its Binary Decision Diagram (BOD)...
An Engineering Change Methodology using Simulation Relations (2009)
Sunil P. Khatri, Amit Narayan, Sriram C. Krishnan, Robert K. Brayton
Abstract In this paper, we address the problem of Engineering Change in a non-deterministic finite state machine framework. We are given a deterministic implementation FSM, and a non-deterministic...
Clockless Implementation Structure and Methodology for DSM Implementation (2008)
Yinghua Li, Alex Kondratyev, Robert K. Brayton
We explore a new implementation method for clockless designs based on (1) dynamic PLAs, (2) a synchronous design flow, and (3) timing assumptions realistic for DSM technologies. We argue for the...
Conflict-Guided Simplification for SAT (2008)
Sanjit A. Seshia, Alan Mishchenko, Robert K. Brayton
Abstract. Boolean satisfiability (SAT) solvers are the computational engines used in a variety of applications, including verification and synthesis. The NP-completeness of SAT implies that solvers...
Checkerboard: A Regular Structure and its Synthesis (2008)
Abstract — A regular circuit structure called a Checkerboard (CB) is proposed. In some CB configurations, all mask layers except the via layers are pre-designed, which is attractive for high...
Conflict-Guided Simplification for SAT (2008)
Sanjit A. Seshia, Alan Mishchenko, Robert K. Brayton
Abstract. Boolean satisfiability (SAT) solvers are the computational engines for a variety of applications, including those in verification and synthesis. The NP-completeness of SAT implies that...
Using SAT for Combinational Equivalence Checking mukul,brayton¢ (2008)
Evgueni I. Goldberg, Mukul R. Prasad, Robert K. Brayton
This paper addresses the problem of combinational equivalence checking (CEC) which forms one of the key components of the current verification methodology for digital systems. A number of recently...
Abstract On Clustering for Minimum Delay/Area (2008)
Chuck Kring, A. Richard Newton, Rajeev Murgai, Robert K. Brayton, Alberto Sangiovanni-vincentelli
An extension to the Fiduccia and Mattheyses mincut algorithm allows cells to be replicated in both sides of the partition. This technique can substantially reduce the number of cut nets in a...
A Practical Way To Maintain A Transitive Reduction (2008)
Robert K. Brayton, Alan Mishchenko
Abstract — Several authors have studied methods to construct the transitive reduction of a directed graph, but little work has been done on how to maintain it. We are motivated by a real-world...
Abstract A Redesign Technique for Combinational Circuits Based on Gate Reconnections (2008)
Yuji Kukimoto, Masahiro Fujita, Robert K. Brayton
In this paper, we consider a redesign technique applicable to combinational circuits implemented with gate-array or standard-cell technology, where we rectify an existing circuit only by reconnecting...
Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment (2008)
Masahiro Fujita, Hisanori Fujisawa, Nobuaki Kawato, Sharad Malik, Albert R. Wang, Robert K. Brayton, ...
R.E. Bryant proposed a method to handle logic expressions [3], which is based on binary decision diagrams (BDD) with restriction: variable ordering is fixed throughout a diagram. Although the method...
0-89791-993-9/97 $10.00 © 1997 IEEE Reachability Analysis Using Partitioned-ROBDDs (2008)
Amit Narayan, Adrian J. Isles, Jawahar Jain, Robert K. Brayton
In this paper, we addressthe problem of finite state machine (FSM) traversal, a key step in most sequential verification and synthesis algorithms. We propose the use of partitioned-ROBDDs to reduce...
Robert K. Brayton, Alan Mishchenko, Nina Yevtushenko
Introduction to BALM Finite-state automata and their languages are well-studied subjects since the early development of computation theory. Traditional automata manipulations are based on explicit...
Abstract Efficient BDD Algorithms for FSM Synthesis and Verification (2008)
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Bernard Plessier, Carl Pixley
We describe a set of BDD based algorithms for efficient FSM synthesis and verification. We establish that the core computation in both synthesis and verification is forming the image and pre-image of...
General Terms Algorithms Design (2008)
Yunjian Jiang, Slobodan Matic, Robert K. Brayton
Logic evaluation of a Boolean function or relation is traditionally done by simulating its gate-level implementation, or creating a branching program using its Binary Decision Diagram (BDD)...
SAT-based complete don’t-care computation for network optimization (2008)
Alan Mishchenko, Robert K. Brayton
This paper describes an improved approach to Boolean network optimization using internal don’t-cares. The improvements concern the type of don’t-cares computed, their scope, and the computation...
Merging Nodes Under Sequential Observability (2008)
Victor N. Kravets, Alan Mishchenko, Robert K. Brayton
Abstract — This paper presents a new type of sequential technology independent synthesis. Building on the previous notions of combinational observability and sequential equivalence, sequential...
Combinational Verification Based on High-Level Functional Specifications (2008)
Evguenii I. Goldberg, Yuji Kukimoto, Robert K. Brayton
We present a new combinational verification technique where the functional specification of a circuit under verification is utilized to simplify the verification task. The main idea is to assign to...
On Iterative Verification with Timed Automata (2007)
Serdar Tasiran, Robert K. Brayton
A timed automaton is said to have the simple path property (SPP) if any given sequence of states is traversable if and only if it is traversable by a simple path. With this restriction it becomes...
Abstract PLANNING FOR PERFORMANCE (2007)
A shift is proposed in the design of VLSI circuits. In conventional design, higher levels of synthesis produce a netlist, from which layout synthesis builds a mask specification for manufacturing....
A Real-time Decision Diagram for Timing Analysis and Synthesis (2007)
In this paper, we introduce an efficient real-time decision diagram, TBF BDD, characterizing both logical functionality and timing information of circuits. In contrast to the conventional timing...
Timing-Safe False Path Removal for Combinational Modules (2007)
Yuji Kukimoto Robert, Robert K. Brayton
A combinational module is a combinational circuit that can be used under any arrival time condition at the primary inputs. An intellectual property (IP) module, if combinational, is one such example....
A Novel Framework for Solving the State Assignment Problem for Event-Based Specifications (2007)
Luciano Lavagno, Cho W. Moon, Robert K. Brayton, Alberto Sangiovanni-Vincentelli
We propose a novel framework to solve the state assignment problem arising from the signal transition graph (STG) representation of an asynchronous circuit. We first establish a relation between STGs...
Combining Top-down and Bottom-up approaches for ROBDD Construction (2007)
Jawahar Jain, Amit Narayan, Claudionor Coelho, Sunil P. Khatri, Robert K. Brayton, Masahiro Fujita
ROBDDs have traditionally been built in a bottom-up fashion, through the recursive use of Bryant's apply procedure [6], or the ITE [4] procedure. With these methods, the peak memory utilization...
Using SAT for Combinational Equivalence Checking mukul,brayton¢ (2007)
Evgueni I. Goldberg, Mukul R. Prasad, Robert K. Brayton
This paper addresses the problem of combinational equivalence checking (CEC) which forms one of the key components of the current verification methodology for digital systems. A number of recently...
Nina Yevtushenko, Robert K. Brayton, Alex Petrenko
The problem of designing a component that combined with a known part of a system, conforms to a given overall specification arises in several applications ranging from logic synthesis to the design...
Abstract A Novel VLSI Layout Fabric for Deep Sub-Micron Applications (2007)
Sunil P. Khatri, Amit Mehrotra, Robert K. Brayton, Alberto Sangiovanni-vincentelli
We propose a new VLSI layout methodology which addresses the main problems faced in Deep Sub-Micron (DSM) integrated circuit design. Our layout “fabric ” scheme eliminates the conventional notion...
Equisolvability of Series vs. Controller's Topology in Synchronous Language Equations (2007)
Nina Yevtushenko, Tiziano Villa, Robert K. Brayton, Alex Petrenko
Given a plant MA and a specification MC, the largest solution of the FSM equation MX
Evguenii I. Goldberg, Luca P. Carloni, Robert K. Brayton
We introduce a new technique to solve exactly a discrete optimization problem, based on the paradigm of "negative " thinking. The motivation is that when searching the space of...
Retiming and resynthesis: A complexity perspective (2006)
Abstract—Transformations using retiming and resynthesis operations are the most important and practical (if not the only) techniques used in optimizing synchronous hardware systems. Although these...
SAT-Based Complete Don't-Care Computation for Network Optimization (2005)
Mishchenko, Alan, Brayton, Robert K.
This paper describes an improved approach to Boolean network optimization using internal don't-cares. The improvements concern the type of don't-cares computed, their scope, and the computation...
SAT-Based Complete Don't-Care Computation for Network Optimization (2005)
Mishchenko, Alan, Brayton, Robert K.
This paper describes an improved approach to Boolean network optimization using internal don't-cares. The improvements concern the type of don't-cares computed, their scope, and the computation...
Functional dependency for verification reduction (2004)
Abstract. The existence of functional dependency among the state variables of a state transition system was identified as a common cause of inefficient BDD representation in formal verification....
SPFD-based wire removal in standard-cell and network-of-PLA circuits (2004)
Sunil P. Khatri, Subarnarekha Sinha, Robert K. Brayton
Abstract—Wire removal is a technique by which the total number of wires between individual circuit nodes is reduced, either by removing wires or replacing them with other new wires. The wire...
Don’t cares in logic minimization of extended finite state machines (2003)
Yunjian Jiang, Robert K. Brayton
been proposed to model control oriented systems. A version of this, with the data portion modeled by Presburger arithmetic, has been used in formal verification and test pattern generation. This...
Equisolvability of Series vs. Controller's Topology in Synchronous Language Equations (2003)
Nina Yevtushenko, Tiziano Villa, Robert K. Brayton, Alex Petrenko
the largest solution of the FSM equation on 21884 - contains all possible discrete controllers . Often we are interested in computing the complete solutions whose composition with the plant is...
Fishbone: A Block-Level Placement and Routing Scheme (2003)
A block-level placement and routing scheme called Fishbone is presented. The routing uses a two-layer spine topology. The pin locations are configurable and restricted to certain routing grids in...
Generalized cofactoring for logic function evaluation (2003)
Yunjian Jiang, Slobodan Matic, Robert K. Brayton
Abstract — Logic evaluation of a Boolean function or relation is traditionally done by simulating its gate-level implementation, or creating a branching program using its Binary Decision Diagram...
Software synthesis from synchronous specifications using logic simulation techniques (2002)
Yunjian Jiang, Robert K. Brayton
This paper addresses the problem of automatic generation of implementation software from high-level functional specifications in the context of embedded system on chip designs. Software design...
Software synthesis from synchronous specifications using logic simulation techniques (2002)
Yunjian Jiang, Robert K. Brayton
This paper addresses the problem of automatic generation of implementation software from high-level functional specifications in the context of embedded system on chip designs. Software design...
Massimo Baleani, Frank Gennari, Yunjian Jiang, Yatish Patel, Robert K. Brayton, Alberto Sangiovanni-vincentelli
This paper studies the usage of a reconfigurable architecture platform for embedded control applications aimed at improving real time performance. The hw/sw codesign methodology from POLIS is used....
Massimo Baleani, Frank Gennari, Yunjian Jiang, Yatish Patel, Robert K. Brayton, Alberto Sangiovanni-vincentelli
This paper studies the use of a reconfigurable architecture platform for embedded control applications aimed at improving real time performance. The hw/sw codesign methodology from POLIS is used. It...
Whirlpool PLAs: a regular logic structure and their synthesis (2002)
Abstract ⎯ A regular circuit structure called a Whirlpool PLA (WPLA) is proposed. It is suitable for the implementation of finite state machines as well as combinational logic. A WPLA is logically...
Massimo Baleani, Frank Gennari, Yunjian Jiang, Yatish Patel, Robert K. Brayton, Alberto Sangiovanni-vincentelli
This paper studies the usage of a reconfigurable architecture platform for embedded control applications aimed at improving real time performance. The hw/sw codesign methodology from POLIS is used....
A Boolean Paradigm in Multi-Valued Logic Synthesis (2002)
Alan Mishchenko Robert, Robert K. Brayton
Optimization algorithms used in binary multi-level logic synthesis, such as network simplification, logic extraction, and resubstitution, have been treated independently and did not share...
Higher-Order Flexibilities in Multi-Valued Networks (2002)
Alan Mishchenko, Robert K. Brayton
Computation of complete flexibility (CF) of a node in the non-deterministic MV network is introduced in [10]. CF describes the freedom to modify a node without violating the functionality of the...
Software synthesis from synchronous specifications using logic simulation techniques (2002)
Yunjian Jiang, Robert K. Brayton
This paper addresses the problem of automatic generation of implementation software from high-level functional specifications in the context of embedded system on chip designs. Software design...
Whirlpool PLAs: a regular logic structure and their synthesis (2002)
Abstract ⎯ A regular circuit structure called a Whirlpool PLA (WPLA) is proposed. It is suitable for the implementation of finite state machines as well as combinational logic. A WPLA is logically...
Massimo Baleani, Frank Gennari, Yunjian Jiang, Yatish Patel, Robert K. Brayton, Alberto Sangiovanni-vincentelli
This paper studies the use of a reconfigurable architecture platform for embedded control applications aimed at improving real time performance. The hw/sw codesign methodology from POLIS is used. It...
Cross-Talk Noise Immune VLSI Design Using Regular Layout Fabrics (2001)
Khatri, Sunil P., Brayton, Robert K., Sangiovanni-Vincentelli, Alberto
Cross-Talk Noise Immune VLSI Design Using Regular Layout Fabrics (2001)
Khatri, Sunil P., Brayton, Robert K., Sangiovanni-Vincentelli, Alberto
0-7923-7407-X
Negative Thinking in Branch-and-Bound: the Case of Unate Covering (2000)
Evguenii I. Goldberg, Luca P. Carloni, Student Member, Tiziano Villa, Robert K. Brayton
Abstract—We introduce a new technique for solving some discrete optimization problems exactly. The motivation is that when searching the space of solutions by a standard branch-and-bound (B&B)...
Cross-talk immune VLSI design using a network of PLAs embedded in a regular layout fabric (2000)
Sunil P. Khatri, Robert K. Brayton, Alberto Sangiovanni-vincentelli
We present a VLSI design methodology to address the cross-talk problem, which is becoming increasingly important in Deep Sub-Micron (DSM) IC design. In our approach, we implement the logic netlist in...
Binary and multivalued SPFD-based wire removal (2000)
Subarnarekha Sinha, Sunil P. Khatri, Robert K. Brayton
This paper describes the application of binary and multivalued SPFD-based wire removal techniques for circuit implementations utilizing networks of PLAs. It has been shown that a design style based...
Negative Thinking in Branch-and-Bound: the Case of Unate Covering (2000)
Evguenii I. Goldberg, Luca P. Carloni, Tiziano Villa, Robert K. Brayton
Abstract | We introduce a new technique for solving some discrete optimization problems exactly. The motivation is that when searching the space of solutions by a standard Branch-and-Bound (B&B)...
Sequential synthesis using s1s (2000)
Adnan Aziz, Felice Balarin, Robert K. Brayton, Alberto Sangiovanni-vincentelli
Abstract—We propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this leads to simple and mathematically elegant...
Integration of Retiming with Architectural Floorplanning (2000)
Abdallah Tabbara, Bassam Tabbara, Robert K. Brayton, A. Richard Newton
The concept of improving the timing behavior of a circuit by relocating registers is called retiming and was first presented by Leiserson and Saxe. They showed that the problem of determining an...
Sequential multi-valued network simplification using redundancy removal (1999)
Sunil P Khatri, Robert K Brayton
We introduce a scheme to simplify a multi-valued network using redundancy removal techniques. Recent methods [1], [2] for binary redundancy removal avoid the use of state traversal. Additionally, [2]...
Sequential multi-valued network simplification using redundancy removal (1999)
Sunil P. Khatri, Robert K. Brayton
We introduce a scheme to simplify a multi-valued network using redundancy removal techniques. Recent methods [1], [2] for binary redundancy removal avoid the use of state traversal. Additionally, [2]...
Retiming for DSM with Area-Delay Trade-offs and Delay Constraints (1999)
Abdallah Tabbara, Robert K. Brayton, A. Richard Newton
The concept of improving the timing behavior of a circuit by relocating registers is called retiming and was first presented by Leiserson and Saxe. They showed that the problem of determining an...
Using Combinational Verification for Sequential Circuits (1999)
Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton
Retiming combined with combinational optimization is a powerful sequential synthesis method. However, this methodology has not found wide application because formal sequential verification is not...
AURA II: Combining Negative Thinking and Branch-And-Bound in Unate Covering Problems (1999)
Luca P. Carloni, Evguenii I. Goldberg, Tiziano Villa, Robert K. Brayton
Recently a novel technique has been published to augment traditional Branch-and-Bound (B&B) while solving exactly a discrete optimization problem [Goldberg et al., 1997]. This technique is based...
Using Combinational Verification for Sequential Circuits (1999)
Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton
Retiming combined with combinational optimization is a powerful sequential synthesis method. However, this methodology has not found wide application because formal sequential verification is not...
SPFD-based Wire Removal in a Network of PLAs (1999)
Sunil P. Khatri, Subarnarekha Sinha, Andreas Kuehlmann, Robert K. Brayton, Alberto Sangiovanni-Vincentelli
This paper describes the application of an SPFD-based wire removal technique for circuit implementations utilizing networks of PLAs. It has been shown that a design style based on a multi-level...
Wireplanning in Logic Synthesis (1998)
Wilsin Gosti, Amit Narayan, Robert K. Brayton
In this paper, we propose a new logic synthesis methodology to deal with the increasing importance of the interconnect delay in deepsubmicron technologies. We first show that conventional logic...
Wireplanning in Logic Synthesis (1998)
Wilsin Gosti, Amit Narayan, Robert K. Brayton
In this paper, we propose a new logic synthesis methodology to deal with the increasing importance of the interconnect delay in deep-submicron technologies. We analyze an example to show why the...
Wireplanning in Logic Synthesis (1998)
Wilsin Gosti, Amit Narayan, Robert K. Brayton
In this paper, we propose a new logic synthesis methodology to deal with the increasing importance of the interconnect delay in deepsubmicron technologies. We first show that conventional logic...
On the optimization power of retiming and resynthesis transformations (1998)
Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton
Retiming and resynthesis transformations can be used for optimizing the area, power, and delay of sequential circuits. Even though this technique has been known for more than a decade, its exact...
Hierarchical Functional Timing Analysis (1998)
Yuji Kukimoto, Robert K. Brayton
We propose a hierarchical timing analysis technique for combinational circuits under the tightest known sensitization criterion, the XBD0 delay model. Given a hierarchical combinational circuit, a...
Delay-optimal technology mapping by DAG covering (1998)
Yuji Kukimoto, Robert K. Brayton, Prashant Sawkar
We propose an algorithm for minimal-delay technology mapping for library-based designs. We show that subject graphs need not be decomposed into trees for delay minimization; they can be mapped...
Delay Characterization of Combinational Modules (1998)
Yuji Kukimoto, Robert K. Brayton
We address three related issues on timing characterization of combinational modules. We first introduce a new notion called timing safe-replaceability as a way of comparing the timing characteristics...
Implementation and Use of SPFDs in Optimizing Boolean Networks (1998)
Subarnarekha Sinha Robert, Robert K. Brayton
Yamashita et. al.[1] introduced a new category for expressing the flexibility that a node can have in a multi-level network. Originally presented in the context of FPGA synthesis, the paper has wider...
Delay-Optimal Technology Mapping by DAG Covering (1998)
Yuji Kukimoto Robert, Robert K. Brayton, Prashant Sawkar
We propose an algorithm for minimal-delay technology mapping for library-based designs. We show that subject graphs need not be decomposed into trees for delay minimization; they can be mapped...
On the Optimization Power of Retiming and Resynthesis Transformations (1998)
Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton
Retiming and resynthesis transformations can be used for optimizing the area, power, and delay of sequential circuits. Even though this technique has been known for more than a decade, its exact...
Hierarchical Functional Timing Analysis (1998)
Yuji Kukimoto Robert, Robert K. Brayton
We propose a hierarchical timing analysis technique for combinational circuits under the tightest known sensitization criterion, the XBD0 delay model. Given a hierarchical combinational circuit, a...
Delay-Optimal Technology Mapping by DAG Covering (1998)
Yuji Kukimoto, Robert K. Brayton, Prashant Sawkary
We propose an optimal algorithm for delay minimal technology mapping for library-based designs. We show that subject graphs need not be decomposed into trees for delay minimization; they can be...
Delay Characterization of Combinational Modules by Functional Arrival Time Analysis (1998)
Yuji Kukimoto, Robert K. Brayton
A combinational module is a combinational circuit that can be used under any arrival time condition. In [8] we showed that exact false-path-aware delay characterization of a combinational module can...
Delay-Optimal Technology Mapping by DAG Covering (1998)
Yuji Kukimoto, Robert K. Brayton, Prashant Sawkar
We propose an algorithm for minimal-delay technology mapping for library-based designs. We show that subject graphs need not be decomposed into trees for delay minimization; they can be mapped...
Delay-optimal technology mapping by DAG covering (1998)
Yuji Kukimoto, Robert K. Brayton, Prashant Sawkar
We propose an algorithm for minimal-delay technology mapping for library-based designs. We show that subject graphs need not be decomposed into trees for delay minimization; they can be mapped...
Hierarchical Functional Timing Analysis (1998)
Yuji Kukimoto, Robert K. Brayton
We propose a hierarchical timing analysis technique for combinational circuits under the tightest known sensitization criterion, the XBD0 delay model. Given a hierarchical combinational circuit, a...
On the optimization power of retiming and resynthesis transformations (1998)
Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton
Retiming and resynthesis transformations can be used for optimizing the area, power, and delay of sequential circuits. Even though this technique has been known for more than a decade, its exact...
Rajeev K. Ranjan, Wilsin Gosti, Robert K. Brayton, Alberto Sangiovanni-vincentelli
The breadth-first manipulation technique has proven effective in dealing with very large sized BDDs. However, till now the lack of dynamic variable reordering has remained an obstacle in its...
Exact required time analysis via false path detection (1997)
Yuji Kukimoto, Robert K. Brayton
This paper addresses how to compute required times at intermediate nodes in a combinational network given required times at primary outputs. The simplest approach is to compute them based on...
Canonical TBDD's and Their Application to Combinational Verification (1997)
Evguenii I. Goldberg, Yuji Kukimoto, Robert K. Brayton
We propose a new class of decision diagrams called canonical cube transformation binary decision diagrams (canonical TBDD's), which is an extension of TBDD's proposed by Meinel et al [11,...
Exact Required Time Analysis via False Path Detection (1997)
Yuji Kukimoto, Robert K. Brayton
This paper addresses how to compute required times at intermediate nodes in a combinational network given required times at primary outputs. The simplest approach is to compute them based on...
Exact Required Time Analysis via False Path Detection (1997)
Yuji Kukimoto Robert, Robert K. Brayton
This paper addresses how to compute required times at intermediate nodes in a combinational network given required times at primary outputs. The simplest approach is to compute them based on...
Removing False Paths from Combinational Modules (1997)
Yuji Kukimoto Robert, Robert K. Brayton
The existence of false paths complicates the task of accurate timing analysis significantly. A technique to remove false paths from a combinational circuit without degrading its performance has a...
Hierarchical Timing Analysis under the XBD0 Model (1997)
Yuji Kukimoto Robert, Robert K. Brayton
We propose a hierarchical timing analysis technique applicable to the XBD0 delay model, which is the underlying model for floating mode analysis and viability analysis. Given a hierarchical...
STARI: A Case Study in Compositional and Hierarchical Timing Verification (1997)
Serdar Tasiran, Robert K. Brayton
. In [TAKB96], we investigated techniques for checking if one real-time system correctly implements another and developed theory for hierarchical proofs and assume-guarantee style reasoning. In this...
Minimal Logic Re-Synthesis For Engineering Change (1997)
Gitanjali Swamy, Sriram Rajamani, Chris Lennard, Robert K. Brayton
Introduction Logic synthesis refers to the process of optimizing a logic description of a circuit, given as a net-list of logic (boolean) gates [8]. This representation can be optimized for...
Computing Delay with Coupling Using Timed Automata (1997)
Serdar Tasiran, Yuji Kukimoto, Robert K. Brayton
ion corresponds to overapproximating F . (ii) Image computation is performed by "propagating wavefronts" across the partitions. This corresponds to performing the composition of the...
Negative thinking by incremental problem solving: Application to unate covering (1997)
Evguenii I. Goldberg, Luca P. Carloni, Tiziano Villa, Robert K. Brayton
We introduce a new technique to solve exactly a discrete optimization problem, based on the paradigm of “negative ” thinking. The motivation is that when searching the space of solutions, often a...
Computing Delay with Coupling using Timed Automata (1997)
Yuji Kukimoto, Robert K. Brayton
Deep sub-micron circuits place new requirements on timing analysis tools: More accuracy is needed and new effects such as pattern dependent delays and cross-talk must be modeled. We propose a...
Vis: A system for verification and synthesis (1996)
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-vincentelli, Fabio Somenzi, Adnan Aziz, Szu-tsung Cheng, ...
Sunil Khatri Yuji Kukimoto Abelardo Pardo y Shaz Qadeer Rajeev K. Ranjan
Vis: A system for verification and synthesis (1996)
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-vincentelli, Fabio Somenzi, Adnan Aziz, Szu-tsung Cheng, ...
Sunil Khatri Yuji Kukimoto Abelardo Pardo y Shaz Qadeer Rajeev K. Ranjan
Vis: A system for verification and synthesis (1996)
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-vincentelli, Fabio Somenzi, Adnan Aziz, Szu-tsung Cheng, ...
Sunil Khatri Yuji Kukimoto Abelardo Pardo y Shaz Qadeer Rajeev K. Ranjan
High Performance BDD Package Based on Exploiting Memory Hierarchy (1996)
Rajeev Ranjan, Jagesh V. Sanghavi, Robert K. Brayton, Alberto Sangiovanni-vincentelli
The success of binary decision diagram (BDD) based algorithms for synthesis and/or verification depend on the availability of a high performance package to manipulate very large BDDs. State-ofthe...
Latch Redundancy Removal Without Global Reset (1996)
Shaz Qadeer, Robert K. Brayton, Vigyan Singhal, Carl Pixley
For circuits where there may be latches with no reset line, we show how to replace some of them with combinational logic. All previous work in sequential optimization by latch removal assumes a...
VIS: A System for Verification and Synthesis (1996)
Alberto Sangiovanni-Vincentelli, Adnan Aziz, Szu-Tsung Cheng, Stephen Edwards, Sunil Khatri, Yuji Kukimoto, ...
ion Manual abstraction can be performed by giving a file containing the names of variables to abstract. For each variable appearing in the file, a new primary input node is created to drive all the...
Binary Decision Diagrams on Network of Workstations (1996)
Rajeev Ranjan, Jagesh V. Sanghavi, Robert K. Brayton, Alberto Sangiovanni-vincentelli
The success of all binary decision diagram (BDD) based synthesis and verification algorithms depend on the ability to efficiently manipulate very large BDDs. We present algorithms for manipulation of...
Verifying Abstractions of Timed Systems (1996)
Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, Robert K. Brayton
ions of Timed Systems Serdar Ta¸siran ? Rajeev Alur ?? Robert P. Kurshan ?? Robert K. Brayton ? Abstract. Given two descriptions of a real-time system at different levels of abstraction, we consider...
ESPRESSO-SIGNATURE: A New Exact Minimizer for Logic Functions (1996)
Patrick C. Mcgeer, Jagesh V. Sanghavi, Robert K. Brayton
We present a new algorithm for exact two-level logic optimization. We represent a set of primes by the cube of their intersection. Therefore, the unique set of sets of primes which forms the covering...
Analysis Of Combinational Cycles In Sequential Circuits (1996)
Thomas Shiple, Vigyan Singhal, Robert K. Brayton
This paper addresses the analysis of combinational cycles in synchronous, sequential circuits. A circuit that has a combinational cycle does not necessarily have unstable output behavior: the cycle...
Identifying Common Substructure for Incremental Methods (1996)
Stephen A. Edwards, Gitanjali M. Swamy, Robert K. 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 "node" in the...
High Performance BDD Package By Exploiting Memory Hierarchy (1996)
Jagesh Sanghavi, Rajeev K. Ranjan, Robert K. Brayton, Alberto Sangiovanni-vincentelli
The success of binary decision diagram (BDD) based algorithms for verification depend on the availability of a high performance package to manipulate very large BDDs. State-of-the-art BDD packages,...
The Case for Retiming with Explicit Reset Circuitry (1996)
Vigyan Singhal, Sharad Malik, Robert K. Brayton
Retiming is often used to optimize synchronous sequential circuits for area or delay or both. If the latches 1 that are retimed have a hardware reset value, the initial state of the circuit must also...
Analysis of Combinational Cycles in Sequential Circuits (1996)
Thomas R. Shiple, Vigyan Singhal, Robert K. Brayton
This paper addresses the analysis of combinational cycles in synchronous, sequential circuits. A circuit that has a combinational cycle does not necessarily have unstable output behavior: the cycle...
It usually works: The temporal logic of stochastic systems (1995)
Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton
is defined. pCTL expresses quantitative bounds on the probabilities of correct behavior; it can be interpreted over discrete Markov processes. A bisimulation relation is defined on finite Markov...
Efficient BDD Algorithms for FSM Synthesis and Verification (1995)
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Bernard Plessier, Carl Pixley
We describe a set of BDD based algorithms for efficient FSM synthesis and verification. We establish that the core computation in both synthesis and verification is forming the image and pre-image of...
The Validity of Retiming Sequential Circuits (1995)
Vigyan Singhal Carl, Carl Pixley, Richard L. Rudell, Robert K. Brayton
Retiming has been proposed as an optimization step for sequential circuits represented at the net-list level. Retiming moves the latches across the logic gates and in doing so changes the number of...
BDD Minimization by Truth Table Permutations (1995)
Masahiro Fujita Yuji, Yuji Kukimoto, Robert K. Brayton
Bern, Meinel and Slobodova [1] have recently proposed a novel technique called cube transformations to minimize the size of binary decision diagrams. Given a Boolean function, they try to find a...
BDD Minimization by Truth Table Permutations (1995)
Masahiro Fujita Yuji, Yuji Kukimoto, Robert K. Brayton
Bern, Meinel and Slobodova [1] have recently proposed a novel technique called cube transformations to minimize the size of binary decision diagrams. Given a Boolean function, they try to find a...
Incremental Methods for FSM Traversal (1995)
Gitanjali M. Swamy, Robert K. Brayton, Vigyan Singhal
Computing the set of reachablestates of a finite state machine, is an important component of many problems in the synthesis, and formal verification of digital systems. The process of design is...
Incremental Methods for FSM Traversal (1995)
Gitanjali M. Swamy, Vigyan Singhal, Robert K. Brayton
Computing the set of reachable states of a finite state machine, is an important component of many problems in the synthesis, and formal verification of digital systems. Computing the reachable...
The Validity of Retiming Sequential Circuits (1995)
Vigyan Singhal, Carl Pixley, Richard L. Rudell, Robert K. Brayton
Retiming has been proposed as an optimization step for sequential circuits represented at the net-list level. Retiming moves the latches across the logic gates and in doing so changes the number of...
Exploiting Power-up Delay for Sequential Optimization (1995)
Vigyan Singhal, Carl Pixley, Adnan Aziz, Robert K. Brayton
Recent work has identified the notion of safe replacement for sequential synchronous designs that may not have reset hardware or even explicitly known initial states. Safe replacement requires that a...
Power-up Delay for Retiming Digital Circuits (1995)
Vigyan Singhal, Carl Pixley, Robert K. Brayton
Retiming is sometimes used to optimize gate-level sequential designs. This technique allows memory elements to be moved across combinational elements. Unfortunately, retiming may cause the...
The Rabin Index and Chain automata, with applications to automata and games (1995)
Sriram C. Krishnan, Anuj Puri, Robert. K. Brayton, Pravin P. Varaiya
. In this paper we relate the Rabin Index of an !-language to the complexity of translation amongst automata, strategies for two-person regular games, and the complexity of controller-synthesis and...
Timing-Safe Replaceability for Combinational Designs (1995)
Adnan Aziz, Robert K. Brayton, Felice Balarin, Vigyan Singhal
This paper addresses the problem of verifying that a combinational design is a timing-safe replacement for an existing design without making any assumptions about the environment of the design. A...
Incremental Methods for FSM Traversal (1995)
Gitanjali M. Swamy, Vigyan Singhal, Robert K. Brayton
Computing the set of reachable states of a finite state machine is an important component of many problems in the synthesis, and formal verification of digital systems. Computing the reachable states...
Language Containment of Non-Deterministic Omega-Automata (1995)
Serdar Tasiran, Ramin Hojati, Robert K. Brayton
. Algorithms and techniques to determinize and complement !-automata with various forms of fairness constraints are investigated and implemented. A tool-box is constructed by supplementing these...
Multi-level Synthesis for Safe Replaceability (1994)
Carl Pixley, Vigyan Singhal, Adnan Aziz, Robert K. Brayton
We describe the condition that a sequential digital design is a safe replacement for an existing design without making any assumptions about a known initial state of the design or about its...
Performance optimization using exact sensitization (1994)
Alexander Saldanha, Heather Harkness, Patrick C. Mcgeer, Robert K. Brayton
A common approach to performance optimization of circuits focuses on re-synthesis to reduce the length of all paths greater than the desired delay. We describe a new delay optimization procedure that...
BDD variable ordering for interacting finite state machines (1994)
Adnan Aziz, Serdar Tas, Robert K. Brayton
We address the problem of obtaining good variable orderings for the BDD representation of a system of interacting nite state machines (FSMs). Orderings are derived from the communication structure...
Multi-level Synthesis for Safe Replaceability (1994)
Carl Pixley, Vigyan Singhal, Adnan Aziz, Robert K. Brayton
We describe the condition that a sequential digital design is a safe replacement for an existing design without making any assumptions about a known initial state of the design or about its...
Ramin Hojati, Vigyan Singhal, Robert K. Brayton
We present the edge-Streett/edge-Rabin environment for doing verification using language containment. This environment has a number of desirable properties compared with the L-process/L-automaton...
Synthesizing Interacting Finite State Machines (1994)
Adnan Aziz, Felice Balarin, Robert K. Brayton, Alberto Sangiovanni-vincentelli
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...
A Redesign Technique for Combinational Circuits Based on Gate Reconnections (1994)
Yuji Kukimoto Masahiro, Masahiro Fujita, Robert K. Brayton
In this paper, we consider a redesign technique applicable to combinational circuits implemented with gate-array or standard-cell technology, where we rectify an existing circuit only by reconnecting...
Incremental Formal Design Verification (1994)
Gitanjali M. Swamy, Robert K. Brayton
Language containment is a method for design verification that involves checking if the behavior of the system to be verified is a subset of the behavior of its specifications (properties or...
Ramin Hojati, Vigyan Singhal, Robert K. Brayton
We present the edge-Streett/edge-Rabin environment for doing verification using language containment. This environment has a number of desirable properties compared with the L-process/L-automaton...
Adnan Aziz, Vigyan Singhal, Gitanjali M. Swamy, Robert K. Brayton
We address the problem of compositional minimization of collections of interacting finite state machines that arise in the context of formal verification of hardware designs by language containment....
Heuristic Minimization of BDDs Using Don't Cares (1994)
Thomas Shiple, Ramin Hojati, Robert K. Brayton
We present heuristic algorithms for finding a minimum BDD size cover of an incompletely specified function, assuming the variable ordering is fixed. In some algorithms based on BDDs, incompletely...
Efficient Formal Design Verification: Data Structure + Algorithms (1994)
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Bernard Plessier, Carl Pixley
We describe a data structure and a set of BDD based algorithms for efficient formal design verification. We argue that hardware designs should be translated into an intermediate hierarchical netlist...
Compiling Verilog into Automata (1994)
Szu-Tsung Cheng, Robert K. Brayton
ion of Operators : : : : : : : : : : : : : : : : : : : : : : : : : : 40 5.2.3 Table Decomposition for Non-Blocking Assignments : : : : : : : : : : : 40 5.2.4 HSIS System Calls : : : : : : : : : : : :...
Incremental Formal Design Verification (1994)
Gitanjali M. Swamy, Robert K. Brayton
Design verification is the processof ensuring that a designedsystem satisfies its original requirements. Language containment, a method for performing design verification, involves checking if the...
BDD Variable Ordering for Interacting Finite State Machines (1994)
Adnan Aziz, Serdar Tasiran, Robert K. Brayton
We address the problem of obtaining good variable orderings for the BDD representing the transition relation of a system of interacting finite state machines. We obtain orderings based only on the...
Equivalences for fair Kripke structures (1994)
Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton
. We extend the notion of bisimulation to Kripke structures with fairness. We define equivalences that preserve fairness and are akin to bisimulation. Specifically we define an equivalence and show...
BDD Variable Ordering for Interacting Finite State Machines (1994)
Adnan Aziz, Serdar Tasiran, Robert K. Brayton
We address the problem of obtaining good variable orderings for the BDD representation of a system of interacting finite state machines (FSMs). Orderings are derived from the communication structure...
Minimal Logic Re-synthesis (1994)
Gitanjali M. Swamy, Sriram Rajamani, Chris Lennard, Robert K. Brayton
Most problems in logic synthesis are computationally hard, and are solved using heuristics. This often makes algorithms un-stable; if the input is changed slightly, the new result of synthesis can be...
Computing Boolean Expressions with OBDDs (1993)
Thomas R. Shiple, Robert K. Brayton
We present a method to compute the bdd for an arbitrary Boolean expression, where the operands are themselves bdds. Such expressions are usually computed by the successive application of binary...
Multiple Boolean Relations (1993)
Ellen M. Sentovich, Vigyan Singhal, Robert K. Brayton
Flexibility in selecting the Boolean functions to implement a digital circuit has various forms which have been studied in the literature such as don't care conditions, Boolean relations, and...
A New Exact Minimizer for Two-Level Logic Synthesis (1993)
Robert K. Brayton, Patrick C. Mcgeer, Jagesh V. Sanghavi
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...
Heuristic Minimization of Synchronous Relations (1993)
Vigyan Singhal, Yosinori Watanabe, Robert K. Brayton
SynchronousBoolean relations can represent sequential don't care information in synchronous systems. These allow greater flexibility in expressing don't care information than ordinary...
Heuristic Minimization for Synchronous Relations (1993)
Vigyan Singhal, Yosinori Watanabe, Robert K. Brayton
Optimization for synchronous systems is an important problem in logic synthesis. However, the full utilization of don't care information for sequential synthesis is far from being solved....
Verifying Interacting Finite State Machines : Complexity Issues (1993)
Adnan Aziz, Vigyan Singhal, Robert K. Brayton
. In this report we carry out a computational complexity analysis of a simple model of concurrency consisting of interacting finite state machines with fairness constraints (IFSMs). This model is...
SIS: A System for Sequential Circuit Synthesis (1992)
Ellen M. Sentovich, Kanwar Jit Singh, Luciano Lavagno, Cho Moon, Rajeev Murgai, Alexander Saldanha, ...
SIS is an interactive tool for synthesis and optimization of sequential circuits. Given a state transition table, a signal transition graph, or a logic-level description of a sequential circuit, it...
SIS: A System for Sequential Circuit Synthesis (1992)
Ellen M. Sentovich, Kanwar Jit Singh, Luciano Lavagno, Cho Moon, Rajeev Murgai, Alexander Saldanha, ...
SIS is an interactive tool for synthesis and optimization of sequential circuits. Given a state transition table, a signal transition graph, or a logic-level description of a sequential circuit, it...
SIS: A System for Sequential Circuit Synthesis (1992)
Ellen M. Sentovich, Kanwar Jit Singh, Luciano Lavagno, Cho Moon, Rajeev Murgai, Alexander Saldanha, ...
SIS is an interactive tool for synthesis and optimization of sequential circuits. Given a state transition table, a signal transition graph, or a logic-level description of a sequential circuit, it...
SIS: A System for Sequential Circuit Synthesis (1992)
Ellen M. Sentovich, Kanwar Jit Singh, Luciano Lavagno, Cho Moon, Rajeev Murgai, Alexander Saldanha, ...
SIS is an interactive tool for synthesis and optimization of sequential circuits. Given a state transition table, a signal transition graph, or a logic-level description of a sequential circuit, it...
SIS: A System for Sequential Circuit Synthesis (1992)
Ellen M. Sentovich, Kanwar Jit Singh, Luciano Lavagno, Cho Moon, Rajeev Murgai, Alexander Saldanha, ...
SIS is an interactive tool for synthesis and optimization of sequential circuits. Given a state transition table, a signal transition graph, or a logic-level description of a sequential circuit, it...
Automatic Compositional Minimization in CTL Model Checking (1992)
Massimiliano Chiodo, Magneti Marelli Pavia, Thomas R. Shiple, Robert K. Brayton
We describe a method for reducing the complexity of CTL model checking on a system of interacting finite state machines. The method consists essentially of reducing each component machine with...
Simplification of Non-Deterministic Multi-Valued Networks
Alan Mishchenko Robert, Robert K. 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...