# Technical Reports - Robert K. Brayton

Solving Parallel Equations with BALM-II (EECS-2012-181)

G. Castagnetti, M. Piccolo, T. Villa, N. Yevtushenko, A. Mishchenko and Robert K. Brayton

Synthesizing FSMs According to co-bu chi Properties (M05/13)

G. Wang, A. Mishchenko, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Sequential Synthesis by Language Equation solving (M03/9)

N. Yevtushenko, T. Villa, Robert K. Brayton, A. Petrenko and Alberto L. Sangiovanni-Vincentelli

Logical Analysis of Combinational Cycles (M02/21)

T. R. Shiple, Robert K. Brayton, G. Berry and Alberto L. Sangiovanni-Vincentelli

Don't care computation in minimizing extended finite state machines with Presburger arithmetic (M01/35)

Yunjian Jiang and Robert K. Brayton

Algebraic Methods for Multi-Valued Logic (M99/62)

Robert K. Brayton

Don't Care Wires in Logical/Physical Design (M99/52)

P. Chong, Y. Jiang, S. Khatri, S. Sinha and Robert K. Brayton

Binary and Multi-Valued SPFD-Based Wire Removal in PLA Networks (M99/51)

S.P. Khatri, S. Sinha, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A VLSI Design Methodology Using a Network of PLAs Embedded in a Regular Layout Fabric (M99/50)

S.P. Khatri, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

SPFD-Based Wire Removal in a Network of PLAs (M99/17)

S.P. Khatri, S. Sinha, Andreas Kuehlmann, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Multi-Layer Area Routing Methodology Using a Boolean Satisfiability Based Router (M99/16)

Y. Jiang, S.P. Khatri, Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

Routing Techniques for Deep Sub-Micron Technologies (M99/15)

S.P. Khatri, A. Mehrotra, M.R. Prasad, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Layout and Design Methodology for Deep Sub-micron Applications Using Networks of PLAs (M98/68)

S.P. Khatri, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Survey of Multi-valued Synthesis Techniques (M98/61)

Robert K. Brayton and S.P. Khatri

Combinational Verification Revisted (M98/60)

S.P. Khatri, S.C. Krishnan, Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

Accurate Automatic Timing Characterization of Static CMOS Libraries (M98/58)

S.P. Khatri, Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

Multi-Valued Network Compaction Using Redundancy Removal (M98/44)

S.P. Khatri, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

On the Optimization Power of Retiming and Resynthesis Transformations (M98/26)

R.K. Ranjan, V. Singhal, F. Somenzi and Robert K. Brayton

Accurate Timing Analysis in the Presence of Cross-Talk Using Timed Automata (M98/25)

S. Tasiran, S.P. Khatri, S. Yovine, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Noise-Immune VLSI Layout Methodology with Highly Predictable Parasitics (M98/24)

S.P. Khatri, A. Mehrotra, Robert K. Brayton, R.H.J.M. Otten and Alberto L. Sangiovanni-Vincentelli

Using Combinational Verification for Sequential Circuits (M97/77)

R.K. Ranjan, V. Singhal, F. Somenzi and Robert K. Brayton

Delay-Optimal Technology Mapping by DAG Covering (M97/75)

Y. Kukimoto, Robert K. Brayton and P. Sawkar

Deciding State Reachability for Large FSMs (M97/73)

T.R. Shiple, R.K. Ranjan, Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

Automatic State Reduction Techniques for Hardware Systems Modeled Using Uninterpreted Functions and Infinite Memory (M97/53)

R. Hojati, A.J. Isles and Robert K. Brayton

Exact Required Time Analysis via False Path Detection (M97/44)

Y. Kukimoto and Robert K. Brayton

Partial-Order Reduction in Symbolic State Space Exploration (M97/30)

R. Alur, Robert K. Brayton, Thomas A. Henzinger, S. Qadeer and S.K. Rajamani

Reachability Analysis Using Partitioned- ROBDDs (M97/27)

A. Narayan, A.J. Isles, J. Jain, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Multi-Valued Decision Diagrams for Logic Synthesis and Verification (M96/75)

T. Kam, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Theory and Algorithms for Face Hypercube Embedding (M96/74)

E. Goldberg, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Low Power Synthesis via Transparent Latches and Observability Don't Cares (M96/64)

T. Kitahara and Robert K. Brayton

Generation of a Minimal STG from an Implicit Cover (M96/40)

L. Carloni, T. Villa, T. Kam, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Minimal Logic Re-Synthesis (M96/22)

G.M. Swamy, S. Rajamani, C. Lennard and Robert K. Brayton

Identifying Common Substructure for Incremental Methods (M96/21)

S.A. Edwards, G.M. Swamy and Robert K. Brayton

State Minimization of FSM's with Implicit Techniques (M96/17)

T. Villa, T. Kam, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Binary Decision Diagrams on Network of Workstations (M96/9)

J.V. Sanghavi, R.K. Ranjan, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Symbolic Two-Level Minimization (M95/109)

T. Villa, A. Saldanha, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Explicit and Implicit Algorithms for Binate Covering Problems (M95/108)

T. Villa, T. Kam, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Theory and Algorithms for State Minimization of Non-Deterministic FSM's (M95/107)

T. Kam, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Implicit Computation of Compatible Sets for State Minimization of ISFSM's (M95/106)

T. Kam, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

VIS: A System for Verification and Synthesis (M95/104)

The VIS Group, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Overcoming Memory Constraints in ROBDD Construction by Functional Decomposition and Partitioning (M95/91)

A. Narayan, S.P. Khatri, J. Jain, M. Fujita, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

High Performance BDD Package Based on Exploiting Memory Hierarchy (M95/81)

R.K. Ranjan, J.V. Sanghavi, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Decomposition of Multi-Phase Timed Finite State Machines (M95/67)

S-T. Cheng and Robert K. Brayton

Multi-Level Optimization of FSM Networks (M95/66)

H.Y. Wang and Robert K. Brayton

Compositional Techniques for Mixed Bottom-Up/Top-Down Constructions of ROBDDs (M95/51)

A. Narayan, S.P. Khatri, J. Jain, M. Fujita, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

An Engineering Change Methodology Using Simulation Relations (M95/50)

S.P. Khatri, A. Narayan, S.C. Krishnan, K.L. McMillan, Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

Logic Optimization of FSM Networks Using Input Don't Care Sequences (M95/42)

H-Y Wang and Robert K. Brayton

Combining Top-Down and Bottom-Up Approaches for ROBDD Construction (M95/30)

J. Jain, A. Narayan, C. Coelho, S.P. Khatri, Alberto L. Sangiovanni-Vincentelli, Robert K. Brayton and M. Fujita

Implicit State Minimization of Non-Deterministic FSM's (M95/18)

T. Kam, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Methodology for Formal Verification of Real-Time Systems (M95/11)

F. Balarin, Robert K. Brayton, S-T. Cheng, D.A. Kirkpatrick, Alberto L. Sangiovanni-Vincentelli and E.C. Wu

Delaying Safeness for More Flexibility (M95/5)

V. Singhal, C. Pixley, A. Aziz and Robert K. Brayton

Efficient Formal Design Verification: Data Structure + Algorithm (M94/100)

R.K. Ranjan, A. Aziz, Robert K. Brayton, B. Plessier and C. Pixley

A User Friendly Environment for Property Specification (M94/99)

R.K. Ranjan and Robert K. Brayton

Synthesizing Interacting Finite State Machines (M94/96)

A. Aziz and Robert K. Brayton

The Validity of Retiming Sequential Circuits (M94/79)

V. Singhal, C. Pixley, R.L. Rudell and Robert K. Brayton

Formula-Dependent Equivalence for Compositional CTL Model Checking (M94/78)

A. Aziz, T.R. Shiple, V. Singhal, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Incremental Formal Design Verification (M94/76)

G.M. Swamy and Robert K. Brayton

A Comparative Approach to Processor Verification Using Symbolic Model Checking (M94/59)

N. Ishiura and Robert K. Brayton

An Exact Optimization of Two-Level Acyclic Sequential Circuits (M94/48)

E.M. Sentovich and Robert K. Brayton

Compiling Verilog into Automata (M94/37)

S-T. Cheng and Robert K. Brayton

Multi-Level Synthesis for Safe Replaceability (M94/31)

C. Pixley, V. Singhal, A. Aziz and Robert K. Brayton

Permissible Observability Relations in FSM Networks (M94/15)

H-Y. Wang and Robert K. Brayton

Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment (M94/12)

R. Hojati, V. Singhal and Robert K. Brayton

Heuristic Algorithms for Early Quantification and Partial Product Minimization (M94/11)

R. Hojati, S. Krishnan and Robert K. Brayton

Sequential Test Pattern Generation: Using Implicit STG Traversal Techniques to Generate Tests and Identify Redundancies in Sequential Circuits (M94/4)

C. Wawrukiewicz, A. Saldanha, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Computing Boolean Expressions with OBDDs (M93/84)

T.R. Shiple, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Fully Implicit Algorithm for Exact State Minimization (M93/79)

T. Kam, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

BDD Variable Ordering for Interacting Finite State Machines (M93/71)

A. Aziz, S. Tasiran and Robert K. Brayton

Minimizing Interacting Finite State Machines (M93/68)

A. Aziz, V. Singhal, G.M. Swamy and Robert K. Brayton

Input Don't Care Sequences in FSM Networks (M93/64)

H-Y. Wang and Robert K. Brayton

The Maximum Set of Permissible Behaviors for FSM Networks (M93/61)

Y. Watanabe and Robert K. Brayton

Implicit Generation of Compatibles for Exact State Minimization (M93/60)

T. Kam, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A New Approach for the Synthesis of FSM's from Control-Flow Graphs (M93/59)

M. Sekine, T. Villa, K. Goto and Robert K. Brayton

Heuristic Minimization of BDDs, Using Don't Cares (M93/58)

T.R. Shiple, R. Hojati, Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

Verifying Interacting Finite State Machines (M93/52)

A. Aziz, V. Singhal and Robert K. Brayton

Exact Minimum Delay Computation and Clock Frequencies (M93/40)

W.K.C. Lam, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Physically Realizable Gate Models (M93/33)

P.R. Stephan and Robert K. Brayton

Heuristic Minimization for Synchronous Relations (M93/30)

V. Singhal, Y. Watanabe and Robert K. Brayton

Circuit Delay Models and Their Exact Computation Using Timed Boolean Functions (M93/6)

W.K.C. Lam, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Fully Implicit Quine-McCluskey Procedure Using BDD's (M92/127)

G.M. Swamy, P. McGeer and Robert K. Brayton

Delay Fault Coverage, Test Set Size, and Performance Tradeoffs (M92/119)

W.K. Lam, A. Saldanha, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Combinational Test Generation Using Satisfiability (M92/112)

P.R. Stephan, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Graph Algorithms for Efficient Clock Schedule Optimization (M92/79)

N. Shenoy, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Delay Models and Sensitization Criteria in the False Path Problem (M92/63)

P. McGeer, A. Saldanha, P.R. Stephan, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Verification with Timed Automata (M92/58)

W.K.C. Lam and Robert K. Brayton

Exact Delay Computation with Timed Boolean Functions (M92/57)

W.K.C. Lam, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Minimum Cycle Time of Synchronous Circuit with Bounded Delays (M92/56)

W.K.C. Lam, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Automatic Reduction in CTL Compositional Model Checking (M92/55)

M. Chiodo, T.R. Shiple, Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

SIS: A System for Sequential Circuit Synthesis (M92/41)

E.M. Sentovich, K.J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P.R. Stephan, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

A Novel Framework for Solving the State Assignment Problem for Event-Based Specifications (M92/19)

L. Lavagno, C. Moon, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Boolean Matching in Logic Synthesis (M92/15)

H. Savoj, M.J. Silva, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

BLIF-MV: An Interchange Format for Design Verification and Synthesis (M91/97)

Robert K. Brayton, M. Chiodo, R. Hojati, T. Kam, K. Kodandapani, R.P. Kurshan, S. Malik, Alberto L. Sangiovanni-Vincentelli, E.M. Sentovich, T. Shiple, K.J. Singh and H.Y. Wang

Specification, Synthesis and Verification of Hazard-Free Asynchronous Circuits (M91/67)

C.W. Moon, P.R. Stephan and Robert K. Brayton

Preserving Don't Care Conditions During Retiming (M91/2)

E.M. Sentovich and Robert K. Brayton

Multi-Valued Decision Diagrams (M90/125)

T.Y.K. Kam and Robert K. Brayton

A Framework for Satisfying Input and Output Encoding Constraints (M90/110)

A. Saldanha, T. Villa, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Incremental Synthesis for ``Engineering Changes'' (M90/76)

Y. Watanabe and Robert K. Brayton

MIS-MV: Optimization of Multi-Level Logic with Multiple-Valued Inputs (M90/68)

L. Lavagno, S. Malik, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Consistency and Observability Invariance in Multi-Level Logic Synthesis (M89/88)

P. McGeer and Robert K. Brayton

Extended Stuck-Fault Testability for Combinational Networks (M89/87)

R.C. McGeer, Robert K. Brayton, R.L. Rudell and Alberto L. Sangiovanni-Vincentelli

Retiming and Resynthesis: Optimizing Sequential Networks with Combinational Techniques (M89/28)

S. Malik, E.M. Sentovich, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli

Encoding Symbolic Inputs for Multi-Level Logic Implementation (M88/69)

S. Malik, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli