# Faculty Publications - Robert K. Brayton

## Books

- F. Mo and R. K. Brayton,
*Regular Fabrics in Deep Sub-Micron Integrated-Circuit Design*, Boston: Kluwer Academic Publishers, 2004. [abstract] - 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. [abstract] - 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. [abstract] - T. Villa, T. Kam, R. K. Brayton, and A. L. Sangiovanni-Vincentelli,
*Synthesis of Finite State Machines: Logic Optimization*, Boston: Kluwer Academic, 1997. [abstract] - 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. [abstract] - 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. [abstract] - 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. [abstract] - 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. [abstract] - R. K. Brayton and R. Spence,
*Sensitivity and Optimization*, Computer-Aided Design of Electronic Circuits; v. 2, Amsterdam: Elsevier Scientific, 1980. [abstract]

## 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

- 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 Applica- tions 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. [abstract] - 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. [abstract]
- 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, 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, 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, 2001.
- R. K. Brayton, "Algebraic Methods for Multi-Valued Logic," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/62, 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, 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, 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, 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, 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, 1999.
- S. Khatri, R. K. Brayton, A. Mehrotra, A. L. Sangiovanni-Vincentelli, and M. Prasad, "Routing Techniques for Deep Sub-Micron Technologies," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M99/15, 1999.
- 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, 1998.
- 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 1997.
- 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, 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, 1996.
- 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.
- 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 1995. [abstract]
- 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, 1995. [abstract]
- 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, 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, 1995. [abstract]
- 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, 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, 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, 1995.
- 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, 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, 1994.
- A. Aziz and R. K. Brayton, "Synthesizing Interacting Finite State Machines," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/96, 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, 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, 1994.
- G. Swamy and R. K. Brayton, "Incremental Formal Design Verification," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/76, 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, 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, 1994.
- S. Cheng and R. K. Brayton, "Compiling Verilog into Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M94/37, 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, 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, 1994.
- R. Hojatic, 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, 1994. [abstract]
- 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, 1994. [abstract]
- 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, 1994. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- A. Aziz and R. K. Brayton, "Verifying Interacting Finite State Machines," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/52, 1993. [abstract]
- 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, 1993. [abstract]
- P. Stephan and R. K. Brayton, "Physically Realizable Gate Models," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M93/33, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 1993. [abstract]
- 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, 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, 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, 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, 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, 1992.
- W. Lam and R. K. Brayton, "Verification with Timed Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M92/58, 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, 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, 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, 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, 1992. [abstract]
- 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, 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, 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, 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, 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, 1991.
- T. Kam and R. K. Brayton, "Multi-Valued Decision Diagrams," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M90/125, 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, 1990.
- Y. Watanabe and R. K. Brayton, "Incremental Synthesis for ``Engineering Changes''," EECS Department, University of California, Berkeley, Tech. Rep. UCB/ERL M90/76, 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, 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, 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, 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, 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, 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.