Books

• F. Mo and R. K. Brayton, Regular Fabrics in Deep Sub-Micron Integrated-Circuit Design, Boston: Kluwer Academic Publishers, 2004.
• S. P. Khatri, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, Cross-Talk Noise Immune VLSI Design using Regular Layout Fabrics, Boston: Kluwer Academic, 2001.
• T. Kam, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, Synthesis of Finite State Machines: Functional Optimization, Boston, MA: Kluwer Academic Publishers, 1997.
• T. Villa, T. Kam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, Synthesis of Finite State Machines: Logic Optimization, Boston: Kluwer Academic, 1997.
• R. Murgai, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, Logic Synthesis for Field-Programmable Gate Arrays, The Kluwer International Series in Engineering and Computer Science; SECS 324, Boston: Kluwer Academic Publishers, 1995.
• W. K. C. Lam and R. K. Brayton, Timed Boolean Functions: A Unified Formalism for Exact Timing Analysis, The Kluwer International Series in Engineering and Computer Science; SECS 270. VLSI, Computer Architecture and Digital Signal Processing, Boston: Kluwer Academic Publishers, 1994.
• P. C. McGeer and R. K. Brayton, Integrating Functional and Temporal Domains in Logic Design: The False Path Problem and Its Implications, The Kluwer International Series in Engineering and Computer Science; SECS 139, Boston: Kluwer Academic, 1991.
• R. K. Brayton, G. D. Hachtel, C. T. McMullen, and A. L. Sangiovanni-Vincentelli, Logic Minimization Algorithms for VLSI Synthesis, The Kluwer International Series in Engineering and Computer Science, Vol. 2, Boston, MA: Kluwer Academic Publishers, 1984.
• R. K. Brayton and R. Spence, Sensitivity and Optimization, Computer-Aided Design of Electronic Circuits; v. 2, Amsterdam: Elsevier Scientific, 1980.

Book chapters or sections

• J. R. Jiang and R. K. Brayton, "Functional dependency for verification reduction," in Computer Aided Verification: Proc. 16th Intl. Conf. (CAV 2004), R. Alur and D. A. Peled, Eds., Lecture Notes in Computer Science, Vol. 3114, Berlin, Germany: Springer-Verlag, 2004, pp. 268-280.

Articles in journals or magazines

• N. Yevtushenko, T. Villa, R. K. Brayton, A. Petrenko, and A. L. Sangiovanni-Vincentelli, "Compositionally progressive solutions of synchronous FSM equations," Discrete Event Dynamic Systems, vol. 18, no. 1, pp. 51-89, March 2008.
• A. Mishchenko, S. Chatterjee, and R. K. Brayton, "Improvements to technology mapping for LUT-based FPGAs," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 26, no. 2, pp. 240-253, Feb. 2007.
• J. R. Jiang and R. K. Brayton, "Retiming and resynthesis: A complexity perspective," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 12, pp. 2674-2686, Dec. 2006.
• S. Chatterjee, A. Mishchenko, R. K. Brayton, X. Wang, and T. Kam, "Reducing structural bias in technology mapping," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 12, pp. 2984-2903, Dec. 2006.
• A. Mishchenko and R. K. Brayton, "A theory of nondeterministic networks," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 6, pp. 977-999, June 2006.
• A. Mishchenko, J. S. Zhang, S. Sinha, J. R. Burch, R. K. Brayton, and M. Chrzanowska-Jeske, "Using simulation and satisfiability to compute flexibilities in Boolean networks," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 5, pp. 743-755, May 2006.
• S. P. Khatri, S. Sinha, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "SPFD-based wire removal in standard-cell and network-of-PLA circuits," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 23, no. 7, pp. 1020-1030, July 2004.
• A. Tabbara, B. Tabbara, R. K. Brayton, and A. R. Newton, "Integration of retiming with architectural floor planning," Integration, the VLSI J., vol. 29, no. 1, pp. 25-43, March 2000.
• A. A. Malik, R. K. Brayton, A. R. Newton, and A. L. Sangiovanni-Vincentelli, "Two-level minimization of multivalued functions with large offsets," IEEE Trans. Computers, vol. 42, no. 11, pp. 1325-1342, Nov. 1993.
• S. Malik, L. Lavagno, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Symbolic minimization of multilevel logic and the input encoding problem," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 11, no. 7, pp. 825-843, July 1992.
• A. A. Malik, R. K. Brayton, A. R. Newton, and A. L. Sangiovanni-Vincentelli, "Reduced offsets for minimization of binary-valued functions," IEEE Trans. Computer-Aided Design, vol. 10, no. 4, pp. 413-426, April 1991.
• S. Malik, E. M. Sentovich, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Retiming and resynthesis: Optimizing sequential networks with combinational techniques," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 10, no. 1, pp. 74-84, Jan. 1991.
• R. K. Brayton, G. D. Hachtel, and A. L. Sangiovanni-Vincentelli, "Invited Paper: Multilevel logic synthesis," Proc. IEEE, vol. 78, no. 2, pp. 264-300, Feb. 1990.
• R. K. Brayton, R. Rudell, A. L. Sangiovanni-Vincentelli, and A. R. Wang, "MIS: A multiple-level logic optimization system," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. CAD-6, no. 6, pp. 1062-1081, Nov. 1987.
• R. K. Brayton, G. D. Hachtel, and A. L. Sangiovanni-Vincentelli, "A survey of optimization techniques for integrated-circuit design (Invited Paper)," Proc. IEEE, vol. 69, no. 10, pp. 1334-1362, Oct. 1981.

Articles in conference proceedings

• K. Aadithya, S. Ray, P. Nuzzo, A. Mishchenko, R. K. Brayton, and J. Roychowdhury, "ABCD-NL: Approximating Continuous Non-Linear Dynamical Systems using Purely Boolean Models for Analog/Mixed-Signal Verification," in Proc. IEEE Asia South-Pacific Design Automation Conference, 2014.
• M. Case, A. Mishchenko, and R. K. Brayton, "Cut-based inductive invariant computation," in Proc. 17th Intl. Workshop on Logic and Synthesis (IWLS 2008), New York, NY: The Association for Computing Machinery, Inc., 2008.
• A. Mishchenko and R. K. Brayton, "Recording synthesis history for sequential verification," in Proc. 17th Intl. Workshop on Logic and Synthesis (IWLS 2008), New York, NY: The Association for Computing Machinery, Inc., 2008.
• A. Mishchenko, R. K. Brayton, and S. Chatterjee, "Boolean factoring and decomposition of logic networks," in Proc. 17th Intl. Workshop on Logic and Synthesis (IWLS 2008), New York, NY: The Association for Computing Machinery, Inc., 2008.
• A. Mishchenko, M. Case, R. K. Brayton, and S. Jang, "Scalable and scalably-verifiable sequential synthesis," in Proc. 17th Intl. Workshop on Logic and Synthesis (IWLS 2008), New York, NY: The Association for Computing Machinery, Inc., 2008.
• A. Mishchenko, R. K. Brayton, and S. Jang, "Global delay optimization using structural choices," in Proc. 17th Intl. Workshop on Logic and Synthesis (IWLS 2008), New York, NY: The Association for Computing Machinery, Inc., 2008.
• A. P. Hurst, A. Mishchenko, and R. K. Brayton, "Scalable min-register retiming under timing and initializability constraints," in Proc. 45th ACM/IEEE Annual Design Automation Conf. (DAC 2008), New York, NY: The Association for Computing Machinery, Inc., 2008, pp. 534-539.
• M. L. Case, V. N. Kravets, A. Mishchenko, and R. K. Brayton, "Merging nodes under sequential observability," in Proc. 45th ACM/IEEE Annual Design Automation Conf. (DAC 2008), New York, NY: The Association for Computing Machinery, Inc., 2008, pp. 540-545.
• A. Mishchenko, S. Cho, S. Chatterjee, and R. K. Brayton, "Combinational and sequential mapping with priority cuts," in 2007 IEEE/ACM Intl. Conf. on Computer-Aided Design (ICCAD '07) Digest of Technical Papers, Piscataway, NJ: IEEE Press, 2007, pp. 354-361.
• F. Mo and R. K. Brayton, "A simultaneous bus orientation and bused pin flipping algorithm," in 2007 IEEE/ACM Intl. Conf. on Computer-Aided Design (ICCAD '07) Digest of Technical Papers, Piscataway, NJ: IEEE Press, 2007, pp. 386-389.
• M. L. Case, A. Mischenko, and R. K. Brayton, "Automated extraction of inductive invariants to aid model checking," in Proc. 2007 Formal Methods in Computer Aided Design, Los Alamitos, CA: IEEE Computer Society, 2007, pp. 165-172.
• A. P. Hurst, A. Mishchenko, and R. K. Brayton, "Fast minimum-register retiming via binary maximum-flow," in Proc. 2007 Formal Methods in Computer-Aided Design (FMCAD '07), Los Alamitos, CA: IEEE Computer Society, 2007, pp. 181-187.
• A. Mishchenko, R. K. Brayton, J. H. Jiang, and S. Jan, "SAT-based logic optimization and resynthesis," in Proc. 16th Intl. Workshop on Logic and Synthesis, New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 358-364.
• S. Chatterjee, Z. Wei, A. Mishchenko, and R. K. Brayton, "A linear time algorithm for optimum tree placement," in Proc. 16th Intl. Workshop on Logic and Synthesis (IWLS 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 336-342.
• A. Hurst, A. Mishchenko, and R. K. Brayton, "Fast minimum-register retiming via binary maximum-flow," in Proc. 16th Intl. Workshop on Logic and Synthesis (IWLS 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 328-335.
• M. L. Case, A. Mishchenko, and R. K. Brayton, "Automated extraction of inductive invariants to aid model checking," in Proc. 16th Intl. Workshop on Logic and Synthesis (IWLS 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 282-289.
• J. Pistorius, M. Hutton, A. Mishchenko, and R. K. Brayton, "Benchmarking method and designs targeting logic synthesis for FPGAs," in Proc. 16th Intl. Workshop on Logic and Synthesis (IWLS 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 230-237.
• A. Mishchenko, S. Cho, S. Chatterjee, and R. K. Brayton, "Combinational and sequential mapping with priority cuts," in Proc. 16th Intl. Workshop on Logic and Synthesis (IWLS 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 91-98.
• A. Hurst, A. Mishchenko, and R. K. Brayton, "Minimizing implementation costs with end-to-end retiming," in Proc. 16th Intl. Workshop on Logic and Synthesis (IWLS 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 9-16.
• R. K. Brayton and A. Mishchenko, "Sequential rewriting and synthesis," in Proc. 16th Intl. Workshop on Logic and Synthesis (IWLS 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 1-8.
• S. Chatterjee, A. Mishchenko, R. K. Brayton, and A. Kuehlmann, "On resolution proofs for combinational equivalence," in Proc. 44th Annual ACM/IEEE Design Automation Conf. (DAC 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 600-605.
• F. Mo and R. K. Brayton, "Semi-detailed bus routing with variation reduction," in Proc. 2007 Intl. Symp. on Physical Design (ISPD '07), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 143-150.
• T. Villa, S. Zharikova, N. Yevtushenko, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "A new algorithm for the largest compositionally progressive solution of synchronous language equations," in Proc. 17th ACM Great Lakes Symp. on VLSI (GLSVLSI 2007), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 441-444.
• Y. S. Yang, S. Sinha, A. Veneris, and R. K. Brayton, "Automating logic rectification by approximate SPFDs," in Proc. 2007 Asia and South Pacific Design Automation Conf. (ASP-DAC '07), Piscataway, NJ: IEEE Press, 2007, pp. 402-407.
• A. Mishchenko, S. Chatterjee, and R. K. Brayton, "DAG-aware AIG rewriting: A fresh look at combinational logic synthesis," in Proc. IEEE/ACM 43rd Annual Conf. on Design Automation, New York, NY: ACM Press, 2006, pp. 532-535.
• Y. Li, A. Kondratyev, and R. K. Brayton, "Gaining predictability and noise immunity in global interconnects," in Proc. 5th Intl. Conf. on Application of Concurrency to System Design, Los Alamitos, CA: IEEE Computer Society, 2005, pp. 176-185.
• A. Mishchenko and R. K. Brayton, "SAT-based complete don't-care computation for network optimization," in Proc. Design, Automation and Test in Europe, Vol. 1, Los Alamitos, CA: IEEE Computer Society, 2005, pp. 412-417.
• F. Mo and R. K. Brayton, "A timing-driven module-based chip design flow," in Proc. 2004 41st Design Automation Conf., New York, NY: ACM Press, 2004, pp. 67-70.
• Y. Jiang, S. Matic, and R. K. Brayton, "Generalized cofactoring for logic function evaluation," in Proc. 2003 40th Design Automation Conf., Piscataway, NJ: IEEE Press, 2003, pp. 155-158.
• N. Yevtushenko, T. Villa, R. K. Brayton, A. Petrenko, and A. L. Sangiovanni-Vincentelli, "Equisolvability of series vs. controller's topology in synchronous language equations," in Proc. 6th Design, Automation and Test in Europe Conf. and Exhibition (DATE 2003), N. Wehn and D. Verkest, Eds., Los Alamitos, CA: IEEE Computer Society, 2003, pp. 1154-1155.
• M. Baleani, F. Gennari, Y. Jiang, Y. Patel, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "HW/SW Partitioning and Code Generation of Embedded Control Applications on a Reconfigurable Architecture Platform," in Proceedings of the tenth international symposium on Hardware/software codesign, 2002.
• M. Baleani, F. Gennari, Y. Jiang, Y. Patel, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "HW/SW partitioning and code generation of embedded control applications on a reconfigurable architecture platform," in Proc. 10th Intl. Symp. on Hardware/Software Codesign (CODES 2002), New York, NY: ACM Press, 2002, pp. 151-156.
• R. K. Brayton, "Compatible observability don't cares revisited," in IEEE/ACM Intl. Conf. on Computer Aided Design (ICCAD 2001). Digest of Technical Papers, Piscataway, NJ: IEEE Press, 2001, pp. 618-623.
• A. Tabbara, R. K. Brayton, and A. R. Newton, "Retiming for DSM with area-delay trade-offs and delay constraints," in Proc. 36th Design Automation Conf. (DAC 1999), New York, NY: ACM, Inc., 1999, pp. 725-730.
• R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa, "VIS: A system for verification and synthesis," in Lecture Notes in Computer Science: Computer Aided Verification, R. Alur and T. A. Henzinger, Eds., Vol. 1102, London, UK: Springer-Verlag, 1996, pp. 428-432.
• E. M. Sentovich, K. J. Singh, C. Moon, H. Savoj, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Sequential circuit design using synthesis and optimization," in Proc. IEEE 1992 Intl. Conf. on Computer Design: VLSI in Computers and Processors, Los Alamitos, CA: IEEE Computer Society Press, 1992, pp. 328-333.
• A. A. Malik, R. K. Brayton, A. R. Newton, and A. L. Sangiovanni-Vincentelli, "Reduced offsets for two-level multi-valued logic minimization," in Proc. 275h ACM/IEEE Conf. on Design Automation (DAC '90), New York, NY: ACM, Inc., 1990, pp. 290-296.
• M. Beardslee, C. Kring, R. Murgai, H. Savoj, R. K. Brayton, and A. R. Newton, "SLIP: A software environment for System Level Interactive Partitioning," in 1989 IEEE Intl. Conf. on Computer-Aided Design (ICCAD-89). Digest of Technical Papers, Los Alamitos, CA: IEEE Computer Society Press, 1989, pp. 280-283.
• A. A. Malik, R. K. Brayton, A. R. Newton, and A. L. Sangiovanni-Vincentelli, "A modified approach to two-level logic minimization," in 1988 IEEE Intl. Conf. on Computer-Aided Design (ICCAD-88). Digest of Technical Papers, Los Alamitos, CA: IEEE Computer Society Press, 1988, pp. 106-109.
• R. K. Brayton, G. D. Hachtel, L. A. Hemachandra, A. R. Newton, and A. L. Sangiovanni-Vincentelli, "A comparison of logic minimization strategies using ESPRESSO: An APL program package for partitioned logic minimalization," in Proc. 1982 IEEE Intl. Symp. on Circuits and Systems (ISCAS-82), New York, NY: IEEE, 1982, pp. 42-48.
• R. K. Brayton and C. McMullen, "The decomposition and factorization of Boolean expressions," in Proc. 1982 IEEE Intl. Symp. on Circuits and Systems, Vol. 1, New York, NY: IEEE Press, 1982, pp. 49-54.

Technical Reports

• G. Castagnetti, M. Piccolo, T. Villa, N. Yevtushenko, A. Mishchenko, and R. K. Brayton, "Solving Parallel Equations with BALM-II," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2012-181, July 2012.
• G. Wang, A. Mishchenko, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Synthesizing FSMs According to co-bu chi Properties," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M05/13, April 2005.
• N. Yevtushenko, T. Villa, R. K. Brayton, A. Petrenko, and A. L. Sangiovanni-Vincentelli, "Sequential Synthesis by Language Equation solving," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M03/9, April 2003.
• T. R. Shiple, R. K. Brayton, G. Berry, and A. L. Sangiovanni-Vincentelli, "Logical Analysis of Combinational Cycles," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M02/21, June 2002.
• Y. Jiang and R. K. Brayton, "Don't care computation in minimizing extended finite state machines with Presburger arithmetic," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M01/35, Dec. 2001.
• R. K. Brayton, "Algebraic Methods for Multi-Valued Logic," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/62, Dec. 1999.
• P. Chong, Y. Jiang, S. Khatri, S. Sinha, and R. K. Brayton, "Don't Care Wires in Logical/Physical Design," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/52, Nov. 1999.
• S. Khatri, S. Sinha, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Binary and Multi-Valued SPFD-Based Wire Removal in PLA Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/51, Oct. 1999.
• S. Khatri, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "A VLSI Design Methodology Using a Network of PLAs Embedded in a Regular Layout Fabric," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/50, May 1999.
• S. Khatri, S. Sinha, A. Kuehlmann, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "SPFD-Based Wire Removal in a Network of PLAs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/17, March 1999.
• Y. Jiang, S. Khatri, A. L. Sangiovanni-Vincentelli, and R. K. Brayton, "A Multi-Layer Area Routing Methodology Using a Boolean Satisfiability Based Router," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/16, March 1999.
• S. Khatri, A. Mehrotra, M. Prasad, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Routing Techniques for Deep Sub-Micron Technologies," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/15, March 1999.
• R. K. Brayton and S. Khatri, "A Survey of Multi-valued Synthesis Techniques," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/61, Oct. 1998.
• S. Khatri, S. Krishnan, A. L. Sangiovanni-Vincentelli, and R. K. Brayton, "Combinational Verification Revisted," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/60, Oct. 1998.
• S. Khatri, A. L. Sangiovanni-Vincentelli, and R. K. Brayton, "Accurate Automatic Timing Characterization of Static CMOS Libraries," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/58, Oct. 1998.
• S. Khatri, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Multi-Valued Network Compaction Using Redundancy Removal," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/44, June 1998.
• S. Khatri, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "A Layout and Design Methodology for Deep Sub-micron Applications Using Networks of PLAs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/68, May 1998.
• R. Ranjan, V. Singhal, F. Somenzi, and R. K. Brayton, "On the Optimization Power of Retiming and Resynthesis Transformations," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/26, April 1998.
• S. Tasiran, S. Khatri, S. Yovine, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Accurate Timing Analysis in the Presence of Cross-Talk Using Timed Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/25, April 1998.
• S. Khatri, A. Mehrotra, R. K. Brayton, R. Otten, and A. L. Sangiovanni-Vincentelli, "A Noise-Immune VLSI Layout Methodology with Highly Predictable Parasitics," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M98/24, April 1998.
• R. Ranjan, V. Singhal, F. Somenzi, and R. K. Brayton, "Using Combinational Verification for Sequential Circuits," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/77, Oct. 1997.
• Y. Kukimoto, R. K. Brayton, and P. Sawkar, "Delay-Optimal Technology Mapping by DAG Covering," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/75, Oct. 1997.
• T. Shiple, R. Ranjan, A. L. Sangiovanni-Vincentelli, and R. K. Brayton, "Deciding State Reachability for Large FSMs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/73, Aug. 1997.
• Y. Kukimoto and R. K. Brayton, "Exact Required Time Analysis via False Path Detection," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/44, June 1997.
• R. Hojati, A. Isles, and R. K. Brayton, "Automatic State Reduction Techniques for Hardware Systems Modeled Using Uninterpreted Functions and Infinite Memory," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/53, May 1997.
• R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, "Partial-Order Reduction in Symbolic State Space Exploration," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/30, April 1997.
• A. Narayan, A. Isles, J. Jain, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Reachability Analysis Using Partitioned- ROBDDs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M97/27, April 1997.
• T. Kitahara and R. K. Brayton, "Low Power Synthesis via Transparent Latches and Observability Don't Cares," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/64, 1996.
• T. Kam, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Multi-Valued Decision Diagrams for Logic Synthesis and Verification," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/75, Dec. 1996.
• E. Goldberg, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Theory and Algorithms for Face Hypercube Embedding," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/74, Dec. 1996.
• L. Carloni, T. Villa, T. Kam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Generation of a Minimal STG from an Implicit Cover," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/40, June 1996.
• G. Swamy, S. Rajamani, C. Lennard, and R. K. Brayton, "Minimal Logic Re-Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/22, April 1996.
• S. Edwards, G. Swamy, and R. K. Brayton, "Identifying Common Substructure for Incremental Methods," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/21, April 1996.
• T. Villa, T. Kam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "State Minimization of FSM's with Implicit Techniques," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/17, April 1996.
• J. Sanghavi, R. Ranjan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Binary Decision Diagrams on Network of Workstations," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M96/9, Feb. 1996.
• T. Villa, A. Saldanha, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Symbolic Two-Level Minimization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/109, Dec. 1995.
• T. Villa, T. Kam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Explicit and Implicit Algorithms for Binate Covering Problems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/108, Dec. 1995.
• T. Kam, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Theory and Algorithms for State Minimization of Non-Deterministic FSM's," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/107, Dec. 1995.
• T. Kam, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Implicit Computation of Compatible Sets for State Minimization of ISFSM's," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/106, Dec. 1995.
• The VIS Group, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "VIS: A System for Verification and Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/104, Dec. 1995.
• A. Narayan, S. Khatri, J. Jain, M. Fujita, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Overcoming Memory Constraints in ROBDD Construction by Functional Decomposition and Partitioning," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/91, Nov. 1995.
• R. Ranjan, J. Sanghavi, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "High Performance BDD Package Based on Exploiting Memory Hierarchy," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/81, Oct. 1995.
• S. Cheng and R. K. Brayton, "Decomposition of Multi-Phase Timed Finite State Machines," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/67, Sep. 1995.
• H. Wang and R. K. Brayton, "Multi-Level Optimization of FSM Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/66, Aug. 1995.
• A. Narayan, S. Khatri, J. Jain, M. Fujita, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Compositional Techniques for Mixed Bottom-Up/Top-Down Constructions of ROBDDs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/51, June 1995.
• H. Wang and R. K. Brayton, "Logic Optimization of FSM Networks Using Input Don't Care Sequences," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/42, June 1995.
• S. Khatri, A. Narayan, S. Krishnan, K. McMillan, A. L. Sangiovanni-Vincentelli, and R. K. Brayton, "An Engineering Change Methodology Using Simulation Relations," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/50, April 1995.
• J. Jain, A. Narayan, C. Coelho, S. Khatri, A. L. Sangiovanni-Vincentelli, R. K. Brayton, and M. Fujita, "Combining Top-Down and Bottom-Up Approaches for ROBDD Construction," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/30, April 1995.
• T. Kam, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Implicit State Minimization of Non-Deterministic FSM's," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/18, March 1995.
• F. Balarin, R. K. Brayton, S. Cheng, D. Kirkpatrick, A. L. Sangiovanni-Vincentelli, and E. Wu, "A Methodology for Formal Verification of Real-Time Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/11, Feb. 1995.
• V. Singhal, C. Pixley, A. Aziz, and R. K. Brayton, "Delaying Safeness for More Flexibility," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M95/5, Jan. 1995.
• A. Aziz and R. K. Brayton, "Synthesizing Interacting Finite State Machines," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/96, Dec. 1994.
• R. Ranjan, A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley, "Efficient Formal Design Verification: Data Structure + Algorithm," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/100, Oct. 1994.
• R. Ranjan and R. K. Brayton, "A User Friendly Environment for Property Specification," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/99, Oct. 1994.
• V. Singhal, C. Pixley, R. Rudell, and R. K. Brayton, "The Validity of Retiming Sequential Circuits," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/79, Oct. 1994.
• G. Swamy and R. K. Brayton, "Incremental Formal Design Verification," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/76, Aug. 1994.
• N. Ishiura and R. K. Brayton, "A Comparative Approach to Processor Verification Using Symbolic Model Checking," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/59, Aug. 1994.
• E. Sentovich and R. K. Brayton, "An Exact Optimization of Two-Level Acyclic Sequential Circuits," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/48, July 1994.
• A. Aziz, T. Shiple, V. Singhal, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Formula-Dependent Equivalence for Compositional CTL Model Checking," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/78, June 1994.
• S. Cheng and R. K. Brayton, "Compiling Verilog into Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/37, May 1994.
• C. Pixley, V. Singhal, A. Aziz, and R. K. Brayton, "Multi-Level Synthesis for Safe Replaceability," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/31, April 1994.
• R. Hojati, V. Singhal, and R. K. Brayton, "Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/12, March 1994.
• R. Hojati, S. Krishnan, and R. K. Brayton, "Heuristic Algorithms for Early Quantification and Partial Product Minimization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/11, March 1994.
• H. Wang and R. K. Brayton, "Permissible Observability Relations in FSM Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/15, Feb. 1994.
• C. Wawrukiewicz, A. Saldanha, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Sequential Test Pattern Generation: Using Implicit STG Traversal Techniques to Generate Tests and Identify Redundancies in Sequential Circuits," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/4, Feb. 1994.
• T. Shiple, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Computing Boolean Expressions with OBDDs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/84, Dec. 1993.
• T. Kam, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "A Fully Implicit Algorithm for Exact State Minimization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/79, Nov. 1993.
• A. Aziz, S. Tasiran, and R. K. Brayton, "BDD Variable Ordering for Interacting Finite State Machines," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/71, Oct. 1993.
• A. Aziz, V. Singhal, G. Swamy, and R. K. Brayton, "Minimizing Interacting Finite State Machines," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/68, Sep. 1993.
• H. Wang and R. K. Brayton, "Input Don't Care Sequences in FSM Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/64, Aug. 1993.
• Y. Watanabe and R. K. Brayton, "The Maximum Set of Permissible Behaviors for FSM Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/61, Aug. 1993.
• T. Kam, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Implicit Generation of Compatibles for Exact State Minimization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/60, Aug. 1993.
• M. Sekine, T. Villa, K. Goto, and R. K. Brayton, "A New Approach for the Synthesis of FSM's from Control-Flow Graphs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/59, July 1993.
• T. Shiple, R. Hojati, A. L. Sangiovanni-Vincentelli, and R. K. Brayton, "Heuristic Minimization of BDDs, Using Don't Cares," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/58, July 1993.
• A. Aziz, V. Singhal, and R. K. Brayton, "Verifying Interacting Finite State Machines," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/52, July 1993.
• W. Lam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Exact Minimum Delay Computation and Clock Frequencies," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/40, May 1993.
• P. Stephan and R. K. Brayton, "Physically Realizable Gate Models," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/33, May 1993.
• V. Singhal, Y. Watanabe, and R. K. Brayton, "Heuristic Minimization for Synchronous Relations," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/30, April 1993.
• W. Lam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Circuit Delay Models and Their Exact Computation Using Timed Boolean Functions," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/6, Jan. 1993.
• G. Swamy, P. McGeer, and R. K. Brayton, "A Fully Implicit Quine-McCluskey Procedure Using BDD's," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/127, Nov. 1992.
• W. Lam, A. Saldanha, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Delay Fault Coverage, Test Set Size, and Performance Tradeoffs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/119, Oct. 1992.
• P. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Combinational Test Generation Using Satisfiability," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/112, Oct. 1992.
• N. Shenoy, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Graph Algorithms for Efficient Clock Schedule Optimization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/79, Aug. 1992.
• P. McGeer, A. Saldanha, P. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Delay Models and Sensitization Criteria in the False Path Problem," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/63, June 1992.
• W. Lam and R. K. Brayton, "Verification with Timed Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/58, May 1992.
• W. Lam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Exact Delay Computation with Timed Boolean Functions," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/57, May 1992.
• W. Lam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Minimum Cycle Time of Synchronous Circuit with Bounded Delays," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/56, May 1992.
• E. Sentovich, K. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "SIS: A System for Sequential Circuit Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/41, May 1992.
• L. Lavagno, C. Moon, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "A Novel Framework for Solving the State Assignment Problem for Event-Based Specifications," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/19, Feb. 1992.
• H. Savoj, M. Silva, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Boolean Matching in Logic Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/15, Feb. 1992.
• M. Chiodo, T. Shiple, A. L. Sangiovanni-Vincentelli, and R. K. Brayton, "Automatic Reduction in CTL Compositional Model Checking," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/55, Jan. 1992.
• R. K. Brayton, M. Chiodo, R. Hojati, T. Kam, K. Kodandapani, R. Kurshan, S. Malik, A. L. Sangiovanni-Vincentelli, E. Sentovich, T. Shiple, K. Singh, and H. Wang, "BLIF-MV: An Interchange Format for Design Verification and Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M91/97, Nov. 1991.
• C. Moon, P. Stephan, and R. K. Brayton, "Specification, Synthesis and Verification of Hazard-Free Asynchronous Circuits," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M91/67, Aug. 1991.
• E. Sentovich and R. K. Brayton, "Preserving Don't Care Conditions During Retiming," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M91/2, Jan. 1991.
• T. Kam and R. K. Brayton, "Multi-Valued Decision Diagrams," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M90/125, Dec. 1990.
• A. Saldanha, T. Villa, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "A Framework for Satisfying Input and Output Encoding Constraints," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M90/110, Dec. 1990.
• Y. Watanabe and R. K. Brayton, "Incremental Synthesis for ``Engineering Changes''," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M90/76, Aug. 1990.
• L. Lavagno, S. Malik, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "MIS-MV: Optimization of Multi-Level Logic with Multiple-Valued Inputs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M90/68, Aug. 1990.
• P. McGeer and R. K. Brayton, "Consistency and Observability Invariance in Multi-Level Logic Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M89/88, July 1989.
• R. McGeer, R. K. Brayton, R. Rudell, and A. L. Sangiovanni-Vincentelli, "Extended Stuck-Fault Testability for Combinational Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M89/87, July 1989.
• S. Malik, E. Sentovich, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Retiming and Resynthesis: Optimizing Sequential Networks with Combinational Techniques," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M89/28, March 1989.
• S. Malik, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Encoding Symbolic Inputs for Multi-Level Logic Implementation," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M88/69, Nov. 1988.

Patents

• R. K. Brayton, "Character recognition system and method multi-bit curve vector processing," U.S. Patent 4,177,448. Dec. 1979.
• R. K. Brayton, F. G. Gustavson, and G. D. Aachtel, "Tableau network design system," U.S. Patent 3,705,409. Dec. 1972.

Talks or presentations

• A. Tabbara, R. K. Brayton, and A. R. Newton, "Retiming for DSM with area-delay trade-offs and delay constraints," presented at Intl. Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU '99), Monterey, CA, March 1999.