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