%% I have used the following convention: initials are used for %% first and middle names, except when the citation is a PhD thesis, %% in which case the full name is used. %% %% Journals %% @string{iee = "IEE Proc."} @string{spaa = "ACM Symposium in Parallelism in Algorithms and Architecture"} @string{sas = "Static Analysis Symposium"} @string{ipl = "Information Processing Letters"} @string{tc = "IEEE Transactions on Computers"} @string{ieeetc = "IEEE Transactions on Computers"} @string{ieeetcom = "IEEE Transactions on Communications"} @string{ieeeton = "IEEE Transactions on Networking"} @string{ieeecomm = "IEEE Communication Magazine"} @string{jsac = "IEEE Journal on Selected Areas in Communications"} @string{jsl = "Journal of Symbolic Logic"} @string{ieeetcad = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"} @string{springer = "Springer-Verlag"} @string{ire = "IRE Transactions on Electronic Computers"} @string{jetta = "Journal of Electronic Testing: Theory and Applications"} @string{siam_opt = "SIAM Journal of Control and Optimization"} @string{siam = "SIAM"} @string{siam_dm = "SIAM Journal of Discrete Mathematics"} @string{siam_am = "SIAM Journal of Applied Mathematics"} @string{jssc = "IEEE Journal of Solid-State Circuits"} @string{toplas = "ACM Transactions on Programming Languages and Systems"} @string{tocl = "ACM Transactions on Computational Logic"} @string{sigcomm = "ACM SIGCOMM"} @string{sigmetrics = "ACM SIGMETRICS"} @string{todaes = "ACM Transactions on Design Automation of Electronic Systems"} @string{pieee = "Proceedings of the IEEE"} @string{cjtcs = "Chicago Journal of Theoretical Computer Science"} @string{fmsd = "Journal of Formal Methods in System Design"} @string{att = "AT\&T Technical Journal"} @string{fac = "Journal of Formal Aspects of Computing"} @string{jacm = "Journal of the ACM"} @string{cacm = "Communications of the ACM"} @string{iac = "Information and Computation"} %% %% Conf.s %% @string{aaai = "Proceedings of the National Conference on Artificial Intelligence"} @string{vldb = "Proceedings of Conference on Very Large Databases"} @string{cicc = "Proceedings of the Custom Integrated Circuits Conference"} @string{cdc = "Proceedings of the IEEE Conference on Decision and Control"} @string{icalp = "Proceedings of the Colloquium on Automata, Languages, and Programming"} @string{cav = "Computer Aided Verification"} @string{fmcad = "Formal Methods in CAD"} @string{concur = "Proceedings of the Conference on Concurrency"} @string{dac = "Design Automation Conference"} @string{edac = "European Conference on Design Automation"} @string{date = "Design Automation and Test in Europe Conference"} @string{euro-dac = "European Design Automation Conference"} @string{hoti = "Hot Interconnects"} @string{ispled = "International Symposium on Low Power Electronics and Design"} @string{hotchips = "Hot Chips"} @string{iccad = "International Conference on Computer-Aided Design"} @string{iccd = "International Conference on Computer Design"} @string{infocom = "IEEE Infocom"} @string{icc = "IEEE Conference on Communication"} @string{iscas = "International Symposium on Circuits and Systems"} @string{itc = "International Test Conference"} @string{chdl = "Symposium on Computer Hardware Description Languages"} @string{mit6 = "Sixth MIT VLSI Conference"} @string{vlsi = "International Conference on VLSI"} @string{stoc = "ACM Symposium on the Theory of Computing"} @string{focs = "IEEE Symposium on the Foundations of Computer Science"} @string{greatlakes = "Great Lakes Symposium on VLSI"} @string{soda = "Symposium on Discrete Algorithms"} @string{focs = "IEEE Conference on Decision and Control"} @string{lics = "IEEE Symposium on Logic in Computer Science"} @string{popl = "ACM Symposium on Principles of Programming Languages"} @string{lncs = "Lecture Notes in Computer Science"} @string{ieicete = "IEICE Trans. Electron."} @string{vlsitsa = "International Symposium on VLSI Technology, Systems, and Applications"} @string{ispd = "International Symposium on Physical Design"} @string{vlsidesign = "VLSI Design Conference"} @string{osdi = "Symposium on Operating Systems Design and Implementations "} @string{sops = "ACM Symposium on Operating System Principles"} @string{podc = "Principles of Distributed Computing"} @string{vmcai = "Verification, Model Checking, and Abstract Interpretation"} @string{ieeeiscc = "IEEE International Symposium on Computers and Communications"} @string{isscc = "IEEE International Solid State Circuits Conference"} %% %% Universities %% @string{cmu = "Carnegie Mellon University"} @string{mit = "Massachusetts Institute of Technology"} @string{stanford = "Stanford University"} @string{texas = "University of Texas at Austin"} @string{ucb = "The University of California at Berkeley"} @string{erl = "Electronics Research Lab"} @string{src = "Semiconductor Research Corporation"} %% %% Workshops %% @string{iwls = "Proceedings of the International Workshop on Logic Synthesis"} @string{iwmtv = "International Workshop of Microprocessor Test and Verification"} @string{tau = "ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems"} %% %% Reference Categories: %% %% Asynchronous Synthesis %% BDD %% Boolean Relations %% Combinational Logic Optimization %% FPGA %% Initial States %% MIS %% Miscellaneous %% Partitioning %% Performance Optimization %% Pipelines %% PLD %% Retiming %% Sequential Optimization %% SIS %% State Assignment %% State Minimization %% Technology Mapping %% Testing %% Verification %% %% %% Asynchronous Synthesis %% @inproceedings{pan-dac-99, author = {P. Pan}, title = "{Performance-driven Integration of Retiming and Resynthesis}", booktitle = dac, month = jun, year = 1999, pages = {243-246} } @article{brzozowski90, author = {J. A. Brzozowski and C-J. Seger}, title = "{Advances in Asynchronous Circuit Theory -- Part I: Gate and Unbounded Inertial Delay Models}", journal = "Bulletin of the European Association of Theoretical Computer Science", year = 1990, month = oct } @inproceedings{chu92, author = {T. A. Chu}, title = "{Synthesis of Hazard-free Control Circuits from Asynchronous Finite State Machine Specifications}", booktitle = tau, pages = {1-10}, month = mar, year = 1992 } %% Need his full name: @phdthesis{chu_thesis, author = {Tam-Anh Chu}, title = "{Synthesis of Self-timed VLSI Circuits from Graph-theoretic Specifications}", school = mit, year = 1987, month = jun } @inproceedings{kartik-dac-00, author = {J. Jain and D. Moundanos and K. Mohanram and Y. Lu}, title = "{Analysis of Composition, and How to Obtain Smaller Canonical Graphs}", booktitle = dac, month = jun, year = 2000, } @inproceedings{lavagno91, author = {L. Lavagno and K. Keutzer and Sangiovanni-Vincentelli, A. L.}, title = "{Algorithms for Synthesis of Hazard-free Asynchronous Circuits}", booktitle = dac, month = jun, year = 1991, pages = {302-308} } @inproceedings{moon91, author = {C. W. Moon and P. R. Stephan and R. K. Brayton}, title = "{Synthesis of Hazard-free Asynchronous Circuits from Graphical Specifications}", booktitle = iccad, month = nov, year = 1991, pages = {322-325} } @book{unger69, author = {S. H. Unger}, title = "{Asynchronous Sequential Switching Circuits}", publisher = {Wiley Interscience}, year = 1969 } @inproceedings{vanbekbergen91, author = "P. Vanbekbergen and G. Goossens and H. De Man", title = "{A Local Optimization Technique for Asynchronous Control Circuits}", booktitle = iwls, address = {North Carolina}, month = may, year = 1991 } @inproceedings{clarke-88, author = "E. M. Clarke and I. A. Draghicescu", title = "{Expressibility results for linear-time and branching-time logics}", booktitle = "{Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency}", address = "{Noordwijkerhout, Norway}", year = 1988 } %% %% BDD %% @article{hitachi-ptl, author = {D. Lammers}, title = "{Hitachi revives PTL for SH-4}", journal = "{Electronic Engineering Times}", month = jan, year = 1996 } @article{shelah75, author = {S. Shelah}, title = "{The Monadic Theory of Order}", journal = "{Annals of Mathematics}", volume = {102}, pages = {379-419}, year = 1975 } @article{akers78, author = {S. B. Akers}, title = "{Binary Decision Diagrams}", journal = ieeetc, volume = {C-37}, pages = {509-516}, month = jun, year = 1978 } %% BDD reference: @article{bryant86, author = {R. Bryant}, title = "{Graph-based Algorithms for Boolean Function Manipulation}", journal = ieeetc, volume = {C-35}, pages = {677-691}, month = aug, year = 1986 } @inproceedings{jain-iccad-91, author = {Jawahar Jain and Jim Bitner and Donald S. Fussell and Jacob A. Abraham}, title = "{Probabilistic Design Verification}", booktitle = iccad, month = nov, year = 1991 } @inproceedings{bryant-iccad-95, author = {R. Bryant}, title = "{Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification}", booktitle = iccad, month = nov, year = 1995 } @inproceedings{fujita88, author = {M. Fujita and H. Fujisawa and N. Kawato}, title = "{Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams}", booktitle = iccad, pages = {2-5}, month = nov, year = 1988 } @inproceedings{malik88, author = {S. Malik and A. R. Wang and R. K. Brayton and Sangiovanni-Vincentelli, A.}, title = "{Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment}", booktitle = iccad, pages = {6-9}, month = nov, year = 1988 } @techreport{sakurai90, author = "T. Sakurai and B. Lin and A. R. Newton", title = "{Multiple-Output Shared Transistor Logic (MOSTL) Family Synthesized Using Binary Decision Diagrams}", number = "UCB/ERL M90/21", institution = erl, address = {Univ. of California, Berkeley, CA 94720}, month = mar, year = 1990, } @techreport{shiple93b, author = "T. R. Shiple and R. Hojati and Sangiovanni-Vincentelli, A. L. and R. K. Brayton", title = "{Heuristic Minimization of {BDD}s Using Don't Cares}", number = "UCB/ERL M93/58", institution = erl, address = {University of California, Berkeley, CA 94720}, month = jul, year = 1993, } @techreport{TR-SSC, title = "Symbolic Satisfiability Checking for a Theory of Equality", author = "ECE Department --- UT Austin", year = 1997 } @InCollection{BopSip90, author = "R. Boppana and M. Sipser", title = "The Complexity of Finite Functions", booktitle = "Handbook of Theoretical Computer Science, Ed. Jan van Leeuwen (Volume A: Algorithms and Complexity)", volume = "1", publisher = {MIT Press}, year = "1990", } @inproceedings{narayan-iccad-96, author = {A. Narayan and J. Jain and M. Fujita and A. Sangiovanni-Vincentelli}, title = "{Partitioned ROBDDs---A Compact, Canonical and Efficient Manipulable Representation for Boolean Functions}", year = 1996, booktitle = iccad, } @article{flover-99, author = {Rajarshi Mukherjee and Jawahar Jain and Koichiro Takayama and Masahiro Fujita and Jacob A. Abraham and Donald S. Fussell}, title = "An Efficient Filter-Based Approach for Combinational Verification", journal = ieeetcad, volume = "18", number = 11, month = nov, year = 1999, } @article{vanaelten93, author = {Filip Van Aelten and Jonathan Allen and Srinivas Devadas}, title = "Verification of Relations between Synchronous Machines", journal = ieeetcad, volume = "12", number = 12, pages = {1947-1959}, month = dec, year = 1993, keywords = {string function theory}, affiliation = {MIT}, } @inproceedings{hwsw-dac-95, author = {M. Chiodo and P. Giusto and A. Jurecska and L. Lavagno and H. H. Hsieh and K. Suzuki and A. L. Sangiovanni-Vincentelli and E. Sentovitch}, title = "{Synthesis of Software Programs for Embedded Control Applications}", booktitle = dac, address = {San Francisco, CA}, month = jun, year = 1995 } @inproceedings{wilkie-95, author = {A. J. Wilkie}, title = "{On the Decidability of the Real Exponential Field}", booktitle = "{Conference on Order in Algebra and Logic}", address = {Oxford, UK}, year = 1995 } @inproceedings{vardi-database, author = {M. Vardi}, title = "{Non-traditional Applications of Automata Theory}", booktitle = "{Theoretical Aspects of Computer Science}", year = 1994 } @inproceedings{henzinger95, author = {T. Henzinger}, title = "{Hybrid Automata with Finite Bisimulations}", booktitle = icalp, month = jul, address = {Szeged, Hungary}, year = 1995 } @inproceedings{rajeev-dac-96, author = {R. Ranjan and J. Sanghavi and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{High Performance BDD Package Based on Exploiting Memory Hierarchy}", booktitle = dac, month = jun, address = {Las Vegas, NV}, year = 1996 } @inproceedings{shiple93, author = {T. R. Shiple and R. Hojati and A. L. Sangiovanni-Vincentelli and R. K. Brayton}, title = "{Heuristic Minimization of {BDD}s Using Don't Cares}", booktitle = dac, address = {San Diego, CA}, month = jun, year = 1994 } %% MDD reference: @inproceedings{srinivasan90, author = {A. Srinivasan and T. Kam and S. Malik and R. K. Brayton}, title = "{Algorithms for Discrete Function Manipulation}", booktitle = iccad, pages = {92-95}, month = nov, year = 1990 } %% %% Boolean Relations %% @inproceedings{fron94, author = {J. Fron and J. C.-Y. Yang and M. Damiani and G. De Micheli}, title = "{A Synthesis Framework Based on Trace and Automata Theory}", booktitle = iscas, address = {London, UK}, month = may, year = 1994 } @inproceedings{somenzi89, author = {R. K. Brayton and F. Somenzi}, title = "{Minimization of Boolean Relations}", booktitle = iscas, pages = {738-743}, month = may, year = 1989 } @inproceedings{somenzi89a, author = {R. K. Brayton and F. Somenzi}, title = "{Boolean Relations and the Incomplete Specification of Logic Networks}", booktitle = "{Proc. of the Intl. Conf. on VLSI'89}", address = "{Munich}", month = aug, year = 1989 } @inproceedings{somenzi89b, author = {R. K. Brayton and F. Somenzi}, title = "{An Exact Minimizer for Boolean Relations}", booktitle = iccad, pages = {316-319}, month = nov, year = 1989 } @inproceedings{lehman-tcad-97, author = {E. Lehman and Y. Watanabe and J. Grodstein and H. Harkness}, title = "{Logic Decomposition During Technology Mapping}", booktitle = ieeetcad, month = aug, year = 1997 } @inproceedings{lin90a, author = {B. Lin and F. Somenzi}, title = "{Minimization of Symbolic Relations}", booktitle = iccad, pages = {88-91}, month = nov, year = 1990 } @inproceedings{watanabe91a, author = {Y. Watanabe and R. K. Brayton}, title = "{Heuristic Minimization of Boolean Relations}", booktitle = "{Proc. of the MCNC Intl. Workshop on Logic Synthesis}", month = may, volume = 1, year = 1991 } @inproceedings{watanabe91, author = {Y. Watanabe and R. K. Brayton}, title = "{Heuristic Minimization of Multiple-Valued Relations}", booktitle = iccad, pages = {126-129}, month = nov, year = 1991 } @inproceedings{sentovich93, author = {E. M. Sentovich and V. Singhal and R. K. Brayton}, title = "{Multiple Boolean Relations}", booktitle = "{Workshop Notes of the Intl. Workshop on Logic Synthesis}", address = {Tahoe City, CA}, month = may, year = 1993 } %% %% Combinational Logic Optimization %% @manual{benchmarks, author = "R. Lisanke", title = "{Logic Synthesis Benchmark Circuits for the Intl. Workshop on Logic Synthesis}", organization = {Microelectronics Center of North Carolina}, month = may, year = 1989 } @inproceedings{bold, author = {D. Bostick and G. D. Hachtel and R. Jacoby and M. R. Lightner and P. Moceyunas and C. R. Morrison and D. Ravenscroft}, title = "{The Boulder Optimal Logic Design System}", booktitle = iccad, pages = {62-65}, month = nov, year = 1987 } @article{bartlett88, author = {K. A. Bartlett and R. K. Brayton and G. D. Hachtel and R. M. Jacoby and C. R. Morrison and R. L. Rudell and Sangiovanni-Vincentelli, A. L. and A. R. Wang}, title = "{Multilevel Logic Minimization Using Implicit Don't Cares}", journal = ieeetcad, volume = 7, number = 6, pages = {723-740}, month = jun, year = 1988 } @inproceedings{brayton82, author = {R. K. Brayton and C. McMullen}, title = "{The Decomposition and Factorization of Boolean Expressions}", booktitle = iscas, pages = {49-54}, month = may, year = 1982 } @article{yeo-jssc-03, author = {E. Yeo and S. Ausberger and W. Davis and B. Nikolic}, title = "{A 500-Mb/s Soft-Output Viterbi Decoder}", journal = jssc, volume = 38, number = 7, year = 2003 } @article{cam-images, author = {T. Ikenaga and T. Ogura}, title = "{A Fully Parallel 1-Mb CAM LSI for Real-Time Pixel-Parallel Image Processing}", journal = jssc, volume = 35, number = 4, year = 2000 } @article{cerny77, author = {E. Cerny}, title = "{An Approach to Unified Methodology of Combinational Switching Circuits}", journal = ieeetc, volume = 27, number = 8, year = 1977 } @book{hachtel_book, author = {G. D. Hachtel and F. Somenzi}, title = "{Logic Synthesis and Verification Algorithms}", publisher = {Kluwer Academic Publishers}, year = 1996 } @book{espresso, author = {R. K. Brayton and G. D. Hachtel and C. T. McMullen and Sangiovanni-Vincentelli, A. L.}, title = "{Logic Minimization Algorithms for VLSI Synthesis}", publisher = {Kluwer Academic Publishers}, year = 1984 } @inproceedings{malika88, author = {A. Malik and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{A Modified Approach to Two-level Logic Minimization}", booktitle = iccad, pages = {106-109}, month = nov, year = 1988 } @inproceedings{mcgeer89, author = "P. McGeer and R. K. Brayton", title = "{Consistency and Observability Invariance in Multi-Level Logic Synthesis}", booktitle = iccad, pages = {426-429}, month = nov, year = 1989 } %% cspf reference: @inproceedings{muroga89, author = {S. Muroga and Y. Kambayashi and H. C. Lai and J. N. Culliney}, title = "{The Transduction Method - Design of Logic Networks Based on Permissible Functions}", booktitle = ieeetc, month = oct, year = 1989 } @inproceedings{rajski90, author = {J. Vasudevamurthy and J. Rajski}, title = "{A Method for Concurrent Decomposition and Factorization of Boolean Expressions}", booktitle = iccad, pages = {510-513}, month = nov, year = 1990 } @inproceedings{rudell86, author = {R. Rudell and A. Sangiovanni-Vincentelli}, title = "{Exact Minimization of Multiple-Valued Functions}", booktitle = iccad, pages = {352-355}, month = nov, year = 1986 } @article{sapatnekar-tcad-93, author = {S. S. Sapatnekar and V. B. Rao and P. M. Vaidya and S. M. Kang}, title = "{An Exact Solution to the Transistor Sizing Problem for CMOS Circuits using Convex Optimization}", journal = ieeetcad, volume = 11, year = 1993 } @article{mailhot-tcad-93, author = {F. Mailhot and G. De Micheli}, title = "{Algorithms for Technology Mapping Based on Binary Decision Diagrams and on Boolean Operations}", journal = ieeetcad, volume = 12, pages = {599-620}, year = 1993 } @article{rudell87, author = {R. Rudell and A. Sangiovanni-Vincentelli}, title = "{Exact Minimization of Multiple-Valued Functions}", journal = ieeetcad, volume = 5, pages = {727-750}, year = 1987 } @phdthesis{rudell_thesis, author = {Richard L. Rudell}, title = "{Logic Synthesis for VLSI Design}", school = ucb, note = {Memorandum No. UCB/ERL M89/49}, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = apr, year = 1989 } @inproceedings{chaff-dac-01, author = {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and and Sharad Malik}, title = "{CHAFF: Engineering an Efficient SAT Solver.}", booktitle = dac, year = 2001 } @inproceedings{brace90, author = {K. Brace and R. Rudell and R. Bryant}, title = "{Efficient Implementation of a BDD Package}", booktitle = dac, year = 1990 } @inproceedings{vigyan-dac-95, author = {V. Singhal and C. Pixley and R. Rudell and R. Brayton}, title = "{The Validity of Retiming Sequential Circuits}", booktitle = dac, year = 1995 } @inproceedings{saldanha89, author = {A. Saldanha and A. R. Wang and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Multi-Level Logic Simplification using Don't Cares and Filters}", booktitle = dac, pages = {277-282}, year = 1989 } %% Need memorandum number: @phdthesis{savoj_thesis, author = "H. Savoj", title = "{Don't Cares in Multi-Level Network Optimization}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = may, year = 1992 } @inproceedings{savoj90, author = {H. Savoj and R. K. Brayton}, title = "{The Use of Observability and External Don't Cares for the Simplification of Multi-Level Networks}", booktitle = dac, pages = {297-301}, month = jun, year = 1990 } @inproceedings{savoj91c, author = {H. Savoj and R. K. Brayton}, title = "{Observability Relations and Observability Don't Cares}", booktitle = iccad, month = nov, pages = {518-521}, year = 1991 } @inproceedings{savoj91a, author = {H. Savoj and R. K. Brayton and H. Touati}, title = "{Extracting Local Don't Cares for Network Optimization}", booktitle = iccad, month = nov, pages = {514-517}, year = 1991 } @inproceedings{rudell93, author = {R. Rudell}, title = "{Dynamic Variable Ordering for Binary Decision Diagrams}", booktitle = iccad, month = nov, pages = {42-47}, year = 1993 } @inproceedings{fujii93, author = {H. Fujii and G. Ootomo and C. Hori}, title = "{Interleaving Variable Ordering Methods for Ordered Binary Decision Diagrams}", booktitle = iccad, month = nov, pages = {38-41}, year = 1993 } @inproceedings{lin-iccd-91, author = {B. Lin and R. Newton}, title = "{Implicit Manipulation of Equivalence Classes Using Binary Decision Diagrams}", booktitle = iccd, address = {Cambridge, MA}, month = oct, year = 1991 } @inproceedings{geist-fmcad-96, author = {D. Geist and M. Farkas and A. Landver and Y. Lichtenstein and S. Ur and Y. Wolfsthal}, title = "{Coverage Directed Test Generation Using Formal Verification}", booktitle = fmcad, month = nov, year = 1996 } @inproceedings{hoskote96, author = {D. Moundanos and J. Abraham and Y. Hoskote}, title = "{A Unified Framework for Design Validation and Manufacturing Test}", booktitle = itc, year = 1996 } * S. Khurshid, D. Marinov, I. Shlyakhter and D. Jackson. A Case for Efficient Solution Enumeration. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), S. Margherita Ligure, Portofino, Italy. May 2003 @inproceedings{sarfraz-sat-03, author = {S. Khurshid and D. Marinov and I. Shlyakhter and D. Jackson}, title = "{A Case for Efficient Solution Enumeration}", booktitle = "{Theory and Applications of Satisfiability Testing}", month = may, year = 2003 } @inproceedings{dinos95, author = {Y. Hoskote and D. Moundanos and J. Abraham}, title = "{Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors}", booktitle = iccd, address = {Austin, TX}, month = oct, year = 1995 } @inproceedings{kurshan-dac-97, author = {R. Kurshan}, title = "{Formal Verification in a Commercial Setting}", booktitle = dac, month = jun, year = 1997 } @inproceedings{gupta-dac-97, author = {A. Gupta and S. Malik and P. Ashar}, title = "{Towards Formalizing a Validation Methodology Using Simulation Coverage}", booktitle = dac, month = jun, year = 1997 } @inproceedings{mihail-cav-94, author = {M. Mihail and C. Papadimitriou}, title = "{On the Random Walk Method for Protocol Testing}", booktitle = cav, month = jul, year = 1994 } @inproceedings{chan-cav-97, author = {W. Chan and R. Anderson and P. Deame and D. Notkin}, title = "{Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-linear Constraints}", booktitle = cav, month = jul, year = 1997 } @inproceedings{baier-concur-99, author = {Christel Baier and Joost-Pieter Katoen and Holger Hermanns}, title = "{Approximate Symbolic Model Checking of Continuous-Time Markov Chains}", booktitle = concur, year = 1999 } @inproceedings{yuan-iwmtv-98, author = {J. Yuan and K. Shultz and C. Pixley and H. Miller}, title = "{SimGen: A Tool for Automatically Generating Simulation Environments}", booktitle = iwmtv, month = oct, year = 1998 } @inproceedings{ho-iccad-96, author = {R. Ho and M. Horowitz}, title = "{Validation Coverage Analysis for Complex Digital Designs}", booktitle = iccad, month = nov, year = 1996 } @inproceedings{ammann-icfem-98, author = {P. Ammann and P Black and W. Majurski}, title = "{Using Model Checking to Generate Tests from Specifications}", year = 1998, booktitle = {IEEE International Conference on Formal Engineering Methods}, pages = {46-54}, } @inproceedings{dill-isca-95, author = {Richard C. Ho and C. Han Yang and Mark A. Horowitz and David L. Dill}, title = "{Architectural Validation for Processors}", booktitle = "Proceedings of the International Symposium on Computer Architecture", year = 1995 } @inproceedings{devadas-iccad-96, author = {S. Devadas and A. Ghosh and K. Keutzer}, title = "{An Observability-Based Code Coverage Metric for Functional Simulation}", booktitle = iccad, month = nov, year = 1996 } %% %% @inproceedings{watanabe93b, author = {Y. Watanabe and L. Guerra and R. K. Brayton}, title = "{Logic Optimization with Multi-Output Gates}", booktitle = iccd, address = {Boston, MA}, month = oct, pages = {416-420}, year = 1993 } %% %% FPGA %% @inproceedings{kukimoto92, author = {Y. Kukimoto and M. Fujita}, title = "{Rectification Method for Lookup-Table Type FPGA's}", booktitle = iccad, month = nov, pages = {54-61}, year = 1992 } %% %% Initial States %% @inproceedings{pixley91, author = {C. Pixley and G. Beihl}, title = "{Calculating Resetability and Reset Sequences}", booktitle = iccad, pages = {376-379}, month = nov, year = 1991 } @article{cho93, author = {H. Cho and S.-W. Jeong and F. Somenzi and C. Pixley}, journal = jetta, title = "{Synchronizing Sequences and Symbolic Traversal Techniques in Test Generation}", volume = 4, number = 12, pages = {19-31}, year = 1993 } @inproceedings{somenzi93, author = {H. Cho and G. D. Hachtel and E. Macii and B. Plessier and F. Somenzi}, title = "{Algorithms for Approximate FSM Traversal}", booktitle = dac, pages = {25-30}, month = jun, year = 1993, } @article{touati92, author = {H. Touati and R. K. Brayton}, title = "{Computing the Initial States of Retimed Circuits}", journal = ieeetcad, note = {To appear}, month = jul, year = 1992 } %% %% MIS %% @article{mis, author = {R. K. Brayton and R. Rudell and A. L. Sangiovanni-Vincentelli and A. R. Wang}, title = "{MIS: A Multiple-Level Logic Optimization System}", journal = ieeetcad, volume = {CAD-6}, number = 6, pages = {1062-1081}, month = nov, year = 1987 } @inproceedings{savoj91b, author = {H. Savoj and H.-Y. Wang and R. K. Brayton}, title = "{Improved Scripts in MIS-II for Logic Minimization of Combinational Circuits}", booktitle = iwls, address = {North Carolina}, month = may, year = 1991 } %% %% Miscellaneous %% @manual{bds, title = "{VAX DECSIM Reference Manual}", organization = "{Digital Equipment Corporation}", note = {Not generally available.}, month = dec, year = 1985 } @inproceedings{brayton89, author = {R. K. Brayton and F. Somenzi}, title = "{Boolean Relations and the Incomplete Specification of Logic Networks}", booktitle = vlsi, pages = {231-240}, month = aug, year = 1989 } @article{oct_framework, author = {D. Harrison and A. R. Newton and R. Spickelmier and T. J. Barnes}, title = "{Electronic CAD Frameworks}", journal = pieee, volume = 78, number = 2, month = feb, year = 1990 } @proceedings{octtools, editor = {Andrea Casotto}, title = "{Octtools-5.1 Manuals}", organization = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = sep, year = 1991 } @mastersthesis{segal_thesis, author = "Russell Segal", title = "{BDSYN: Logic Description Translator; BDSIM: Switch-Level Simulator}", school = ucb, note = {Memorandum No. UCB/ERL M87/33}, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = may, year = 1987 } @inproceedings{stoelzle89, author = {A. Stoelzle and S. Narayanaswamy and K. Kornegay and H. Murveit and J. Rabaey}, title = "{A VLSI Wordprocessing Subsystem for a Real Time Large Vocabulary Continuous Speech Recognition System}", booktitle = cicc, year = 1989 } %% %% Partitioning %% @inproceedings{silva-date-99, author = {J. P. Silva and T. Glass}, title = "{Combinational Equivalence Checking Using Satisfiability Checking and Recursive Learning}", booktitle = date, month = mar, year = 1999 } @inproceedings{beardslee92, author = {M. Beardslee and B. Lin and A. L. Sangiovanni-Vincentelli}, title = "{Communication Based Logic Partitioning}", booktitle = euro-dac, pages = {32-37}, month = sep, year = 1992 } @article{shannon-bdd, author = {C. E. Shannon}, title = "{The Synthesis of Two-Terminal Switching Circuits}", journal = "Bell System Technical Journal", volume = 28, year = 1949, pages = {59-98} } %% @article{kernighan70, author = {B. W. Kernighan and S. Lin}, title = "{An Efficient Heuristic Procedure for Partitioning Graphs}", journal = "Bell System Technical Journal", volume = 49, year = 1970, pages = {291-307} } %% %% Performance Optimization %% %% speedup reference: @inproceedings{singh88, author = {K. J. Singh and A. R. Wang and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Timing Optimization of Combinational Logic}", booktitle = iccad, year = 1988, pages = {282-285}, month = nov } %% buffer optimization reference: @inproceedings{singh90, author = {K. J. Singh and A. L. Sangiovanni-Vincentelli}, title = "{A Heuristic Algorithm for the Fanout Problem}", booktitle = dac, year = 1990, pages = {357-360}, month = jun } @inproceedings{touati91, author = {H. Touati and H. Savoj and R. K. Brayton}, title = "{Delay Optimization of Combinational Logic Circuits by Clustering and Partial Collapsing}", booktitle = iccad, pages = {188-191}, month = nov, year = 1991 } %% %% Pipelines %% @inproceedings{bose89, author = {S. Bose and A. Fisher}, title = "{Verifying Pipelined Hardware using Symbolic Logic Simulation}", booktitle = iccd, pages = {217-221}, year = 1989 } @book{kogge81, author = {P. M. Kogge}, title = "{The Architecture of Pipelined Computers}", publisher = {Hemisphere Publishing Corporation; McGraw-Hill Book Company}, series = {McGraw-Hill Advanced Computer Science Series}, year = 1981 } %% %% PLD %% @inproceedings{chortle-crf, author = {R. J. Francis and J. Rose and Z. Vranesic}, title = "{Chortle-crf: Fast Technology Mapping for Lookup Table-Based FPGAs}", booktitle = dac, pages = {227-233}, month = jun, year = 1991 } %% Actel reference: @article{yano-jssc-96, author = {K. Yano and Y. Sasaki and K. Rikino and K. Seki}, title = "{Top-Down Pass-Transistor Logic Design}", journal = jssc, month = jun, volume = 31, number = 6, year = 1996, pages = {792-803} } @article{gamal89, author = {A. Gamal et. al.}, title = "{An Architecture for Electrically Configurable Gate Arrays}", journal = jssc, month = apr, volume = 24, number = 2, year = 1989, pages = {394-398} } @article{mathony89, author = {H.-J. Mathony}, title = "{Universal Logic Design Algorithm and its Application to the Synthesis of Two-level Switching Circuits}", journal = iee, month = may, volume = "136 Pt. E", number = 3, year = 1989 } @inproceedings{murgai90, author = {R. Murgai and Y. Nishizaki and N. Shenoy and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Logic Synthesis for Programmable Gate Arrays}", booktitle = dac, month = jun, year = 1990, pages = {620-625} } @inproceedings{murgai-dac-92, author = {R. Murgai and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{An Improved Synthesis Algorithm for Multiplexor-based PGA's}", booktitle = dac, month = jun, year = 1992, pages = {380-386} } @inproceedings{murgai91a, author = {R. Murgai and N. Shenoy and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Improved Logic Synthesis Algorithms for Table Look Up Architectures}", booktitle = iccad, month = nov, year = 1991, pages = {564-567} } @inproceedings{murgai91b, author = {R. Murgai and N. Shenoy and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Performance Directed Synthesis for Table Look Up Programmable Gate Arrays}", booktitle = iccad, month = nov, year = 1991, pages = {572-575} } @inproceedings{roth82, author = {J. P. Roth and R. M. Karp}, title = "{Minimization over Boolean Graphs}", booktitle = "{IBM Journal of Research and Development}", month = apr, year = 1982 } @manual{xilinx, organization = {Xilinx Inc.}, title = "{Xilinx Programmable Gate Array User's Guide}", year = 1988 } %% %% Retiming %% @article{leiserson83a, author = {C. E. Leiserson and J. B. Saxe}, title = "{Optimizing Synchronous Systems}", journal = {Journal of VLSI and Computer Systems}, month = {Spring}, year = 1983, volume = {1}, number = {1}, pages = {41-67} } @inproceedings{leiserson83b, author = {C. E. Leiserson and F. M. Rose and J. B. Saxe}, title = "{Optimizing Synchronous Circuitry by Retiming}", booktitle = "{Advanced Research in VLSI: Proc. of the Third Caltech Conf.}", publisher = {Computer Science Press}, pages = {86-116}, year = 1983 } @techreport{leiserson88, author = {C. E. Leiserson and J. B. Saxe}, title = "{Retiming Synchronous Circuitry}", institution = mit, number = {TM 372, MIT/LCS}, address = {545 Technology Square, Cambridge, Massachusetts 02139}, month = oct, year = 1988 } @phdthesis{saxe_thesis, author = "James B. Saxe", title = "{Decomposable Searching Problems and Circuit Optimization by Retiming: Two Studies in General Transformations of Computational Structures}", school = cmu, note = {CMU-CS-85-162}, address = {Department of Computer Science}, month = aug, year = 1985 } @inproceedings{sentovich91, author = {E. M. Sentovich and R. K. Brayton}, title = "{Preserving Don't Care Conditions During Retiming}", booktitle = vlsi, pages = {461-470}, month = aug, year = 1991 } %% %% Sequential Optimization %% @phdthesis{ashar_thesis, author = "Pranav Ashar", title = "{Synthesis of Sequential Circuits for VLSI Design}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = may, year = 1992 } @inproceedings{damiani92, author = {M. Damiani and De Micheli, G.}, title = "{Synthesis and Optimization of Synchronous Logic Circuits from Recurrence Equations}", booktitle = edac, pages = {226-231}, month = mar, year = 1992 } @inproceedings{chen94, author = {B. Chen and M. Yamazaki and M. Fujita}, title = "{Bug Identification of a Real Chip Design by Symbolic Model Checking}", booktitle = edac, pages = {132-136}, month = mar, year = 1994 } @inproceedings{damiani92a, author = {M. Damiani and De Micheli, G.}, title = "{Recurrence Equations and the Optimization of Synchronous Logic Circuits}", booktitle = dac, pages = {556-561}, month = jun, year = 1992 } @techreport{bryant_tr, author = {M. Starkey and R. E. Bryant}, title = "{sing Ordered Binary-Decision Diagrams for Compressing Images and Image Sequences}", institution = "Carnegie Mellon University", number = {TR-95-105}, address = {Department of Computer Science}, year = 1995, } @techreport{seger93, author = {C.-J. H. Seger and R. E. Bryant}, title = "{Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories}", institution = "University of British Columbia", number = {TR-93-8}, address = {Department of Computer Science}, month = apr, year = 1993 } @techreport{damiani_thesis, author = {M. Damiani and De Micheli, G.}, title = "{Don't care Set Specifications in Combinational and Synchronous Logic Circuits}", institution = stanford, number = {CSL-TR-92-531}, address = {Computer Systems Laboratory, Stanford, CA 94305-4055}, month = jul, year = 1992 } @article{demicheli91, author = {G. DeMicheli}, title = "{Synchronous Logic Synthesis: Algorithms for Cycle-Time Minimization}", journal = ieeetcad, month = jan, volume = 10, pages = {63-73}, number = 1, year = 1991 } @article{devadas89a, author = {S. Devadas and A. R. Newton}, title = "{Decomposition and Factorization of Sequential Finite State Machines}", journal = ieeetcad, volume = {CAD-8}, number = 11, pages = {1206-1217}, month = nov, year = 1989 } @techreport{ bryant94verification, author = "Randy E. Bryant and Yirng-An Chen", title = "Verification of Arithmetic Functions with Binary Moment Diagrams", number = "CS-94-160", pages = "41", year = "1994", url = "citeseer.nj.nec.com/article/bryant95verification.html" } @inproceedings{bryant95, author = {R. Bryant and Y.A. Chen}, title = "{Verification of Arithmetic Circuits with Binary Moment Diagrams}", booktitle = dac, pages = {535-541}, month = jun, year = 1995 } @inproceedings{devadas89b, author = {S. Devadas}, title = "{Approaches to Multi-Level Sequential Logic Synthesis}", booktitle = dac, pages = {270-276}, month = jun, year = 1989 } @book{hartmanis66, author = {J. Hartmanis and R. E. Stearns}, title = "{Algebraic Structure Theory of Sequential Machines}", publisher = {Prentice-Hall}, series = {Intl. Series in Applied Mathematics}, address = {Englewood Cliffs, N.J.}, year = 1966 } @book{kohavi70, author = {Z. Kohavi}, title = "{Switching and Finite Automata Theory}", publisher = {McGraw-Hill Book Company}, series = {Computer Science Series}, year = 1970 } @inproceedings{lin90, author = {B. Lin and H. J. Touati and A. R. Newton}, title = "{Don't Care Minimization of Multi-level Sequential Logic Networks}", booktitle = iccad, pages = {414-417}, month = nov, year = 1990 } @inproceedings{ liao-dac-97, author = "Stan Liao and Srinivas Devadas", title = "Solving Covering Problems Using {LPR}-Based Lower Bounds", booktitle = "Design Automation Conference", pages = "117-120", year = "1997", url = "citeseer.nj.nec.com/liao96solving.html" } @inproceedings{berthet90, author = {C. Berthet and O. Coudert and J. C. Madre}, title = "{New Ideas on Symbolic Manipulation of Finite State Machines}", booktitle = iccd, month = oct, year = 1990 } @inproceedings{lin91, author = {B. Lin and A. R. Newton}, title = "{Exact Redundant State Registers Removal Based on Binary Decision Diagrams}", booktitle = "{Proc. of the MCNC Intl. Workshop on Logic Synthesis}", month = may, volume = 1, year = 1991 } @inproceedings{ms95, author = {P. McGeer and K. McMillan and A. Saldanha and A. Sangiovanni-Vincentelli and P. Scaglia}, title = "{Fast Discrete Function Evaluation}", booktitle = iccad, month = nov, year = 1995 } @inproceedings{ashar95, author = {P. Ashar and S. Malik}, title = "{Fast Functional Simulation Using Branching Programs}", booktitle = iccad, month = nov, year = 1995 } @phdthesis{lin_thesis, author = {Bill Lin}, title = "{Synthesis of VLSI Designs with Symbolic Techniques}", school = ucb, year = 1991, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720} } @phdthesis{malik_thesis, author = {Sharad Malik}, title = "{Combinational Logic Optimization Techniques in Sequential Logic Synthesis}", school = ucb, year = 1990, note = {Memorandum No. UCB/ERL M90/115}, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = nov } @inproceedings{malik90, author = {S. Malik and K. J. Singh and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Performance Optimization of Pipelined Circuits}", booktitle = iccad, pages = {410-413}, month = nov, year = 1990 } @article{malik91, author = {S. Malik and E. M. Sentovich and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Retiming and Resynthesis: Optimization of Sequential Networks with Combinational Techniques}", journal = ieeetcad, month = jan, volume = 10, pages = {74-84}, number = 1, year = 1991 } @article{elgot61, author = { C. C. Elgot}, title = "{ Decision Problems of Finite Automaton Design and Related Decision Problems}", journal = "{Transactions of the American Mathematical Society}", volume = 98, pages = {21-52}, year = 1961 } @inproceedings{buchi61, author = { J. R. Buchi}, title = "{ On a Decision Method in Restricted Second Order Arithmetic}", booktitle = "{International Congress on Logic, Methodology, and Philosophy of Science}", pages = {1-11}, year = 1960 } @book{rabin71, author = {M. O. Rabin}, title = "{Automata on Infinite Objects and Church's Problem}", publisher = "{American Mathematical Society}", year = 1971 } @inproceedings{rho91, author = {J.-K. Rho and G. Hachtel and F. Somenzi}, title = "{Don't Care Sequences and the Optimization of Interacting Finite State Machines}", booktitle = iccad, pages = {418-421}, month = nov, year = 1991 } @article{devadas91b, author = {S. Devadas}, title = "{ Optimizing Interacting Finite State Machines Using Sequential Don't Cares}", journal = ieeetcad, pages = {1473-1484}, month = dec, year = 1991 } @inproceedings{wang93a, author = {H.-Y. Wang and R. K. Brayton}, title = "{Permissible Observability Relations in Interacting Finite State Machines}", booktitle = iwls, address = {Tahoe City, CA}, month = may, year = 1993 } @inproceedings{silva-iwls-99, author = {J. P. Marques-Silva and L. G. Silva}, title = "{Algorithms for Satisfiability Checking in Combinational Circuits based on Backtrack Search and Recursive Learning}", booktitle = iwls, address = {Tahoe City, CA}, month = jun, year = 1999 } @inproceedings{fron93, author = {J. Fron and J. C.-Y. Yang and M. Damiani and G. De Micheli}, title = "{A Synthesis Framework Based on Trace and Automata Theory}", booktitle = iwls, address = {Tahoe City, CA}, month = may, year = 1993 } @inproceedings{wang94a, author = {H.-Y. Wang and R. K. Brayton}, title = "{Permissible Observability Relations in FSM Networks}", booktitle = dac, month = jun, year = 1994 } @inproceedings{wang93b, author = {H.-Y. Wang and R. K. Brayton}, title = "{Input Don't Care Sequences in FSM Networks}", booktitle = iccad, year = 1993 } @article{kim72, author = {J. Kim and M. M. Newborne}, title = "{ The Simplification of Sequential Machines With Input Restrictions}", journal = ire, pages = {1440-1443}, month = dec, year = 1972 } @inproceedings{watanabe93, author = {Y. Watanabe and R. K. Brayton}, title = "{The Maximum Set of Permissible Behaviors for FSM Networks}", booktitle = iccad, year = 1993 } @inproceedings{wolf93, author = {J.R. Burch and D. Dill and E. Wolf and G. DeMicheli}, title = "{Modeling Hierarchical Combinational Circuits}", booktitle = iccad, year = 1993 } @inproceedings{ip93, author = {N. Ip and D. Dill}, title = "{Better Verification Through Symmetry}", booktitle = chdl, year = 1993 } @inproceedings{ravi-iccad-95, author = {K. Ravi and F. Somenzi}, title = "{High Density Reachability Analysis}", month = nov, booktitle = iccad, year = 1995 } @inproceedings{booledozer-iccd-94, author = {D. Brand and R. Damiano and L. van Ginneken and A. Drumm}, title = "{In the driver's seat of BooleDozer}", address = {Boston MA}, month = oct, booktitle = iccd, year = 1994 } @inproceedings{eal-iccad-96, author = {E. A. Lee and L. Sangiovanni-Vincentelli}, title = "{Comparing Models of Computation}", month = nov, booktitle = iccad, year = 1996 } @inproceedings{berlekaar-iccad-95, author = {M. Berlekaar and L. P. P. P. van Ginnekan}, title = "{Efficient Orthonormality Testing for Synthesis with Pass-Transistor Selectors}", address = {Santa Clara, CA}, month = nov, booktitle = iccad, year = 1995 } @inproceedings{silva-iccad-96, author = {J. Silva and K. Sakallah}, title = "{GRASP--A New Search Algorithm For Satisfiability}", address = {Santa Clara, CA}, month = nov, booktitle = iccad, year = 1996 } @inproceedings{detjens-iccad-87, author = {E. Detjens and G. Gannot and R. Rudell and A. Sangiovanni-Vincentelli}, title = "{Technology Mapping in MIS}", address = {Santa Clara, CA}, month = nov, booktitle = iccad, year = 1987 } @inproceedings{singhal93, author = {V. Singhal and Y. Watanabe and R. K. Brayton}, title = "{Heuristic Minimization of Synchronous Relations}", booktitle = iwls, address = {Tahoe City, CA}, month = may, year = 1993 } @inproceedings{berry93, author = {G. Berry and H. J. Touati}, title = "{Optimized Controller Synthesis Using Esterel}", booktitle = iwls, address = {Tahoe City, CA}, month = may, year = 1993 } @techreport{singhal93a, author = {V. Singhal and Y. Watanabe and R. K. Brayton}, title = "{Heuristic Minimization for Synchronous Relations}", institution = erl, number = {UCB/ERL M93/30}, address = {Univ. of California, Berkeley, CA 94720}, year = 1993 } @inproceedings{singhal93b, author = {V. Singhal and Y. Watanabe and R. K. Brayton}, title = "{Heuristic Minimization of Synchronous Relations}", booktitle = iccd, address = {Boston, MA}, month = oct, pages = {428-433}, year = 1993 } @misc{juniper-sms-patent, author = {Juniper Networks}, title = {High Speed Switching Device}, year = 1999, howpublished = "US Patent 5,905,726" } @misc{silva-pc-96, author = {J. Silva}, howpublished = "Personal communication", year = 1996 } @misc{wang93, author = {Huey-Yih Wang}, howpublished = "Personal communication", month = feb, year = 1993 } @misc{york93, author = {Gary York}, howpublished = "Personal communication", month = feb, year = 1993 } %% %% Interacting FSMs for Synthesis/Verification %% @misc{york_pc, author = {Gary York}, howpublished = "{Cadence Design Systems. Personal communication}", year = 1993 } %% @inproceedings{vaandrager91, author = {F. W. Vaandrager}, title = "{On the Relationship Between Process Algebra and Input/Output Automata}", year = 1991, month = jul, booktitle = " IEEE Symposium on Logic in Computer Science", publisher = { IEEE Computer Science Press}, } @inproceedings{rabinovich92, author = {A. Rabinovich}, title = "{Checking Equivalences Between Concurrent Systems of Finite Agents}", series = lncs, volume = 623, year = 1992, month = jul, booktitle = "Proc. Intl. Colloquium on Automata, Languages and Programming (ICALP)", editor = "W. Kuich", publisher = {Springer Verlag}, pages = {696-707} } @article{jones77, author = {Neil D. Jones and Lawrence H. Landweber and Y. Edmund Lien}, title = "{Complexity of some problems in Petri nets}", journal = "{Theoretical Computer Science}", volume = 4, pages = {277-299}, year = 1977 } @inproceedings{lee92, author = { David Lee and Mihalis Yannakakis}, title = "{Online Minimization of Transition Systems}", year = 1992, month = may, booktitle = "ACM Symposium on the Theory of Computation", pages = {264-274}, } @Article{bryant91, author = "R. Bryant", title = "On the Complexity of {VLSI} Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication", journal = "IEEE Transactions on Computers", volume = "40", year = "1991", } @Article{AlpSch87, author = "B. Alpern and F. Schneider", title = "Recognizing Safety and Liveness", journal = "Distributed Computing", volume = "2", year = "1987", } %% %% SIS %% @techreport{sis-erl, author = {E. M. Sentovich and K. J. Singh and L. Lavagno and C. Moon and R. Murgai and A. Saldanha and H. Savoj and P. R. Stephan and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{SIS: A System for Sequential Circuit Synthesis}", institution = erl, number = {UCB/ERL M92/41}, address = {Univ. of California, Berkeley, CA 94720}, month = may, year = 1992 } @inproceedings{sis-iccd, author = {E. M. Sentovich and K. J. Singh and C. Moon and H. Savoj and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Sequential Circuit Design Using Synthesis and Optimization}", booktitle = iccd, pages = {328-333}, month = oct, year = 1992 } @inproceedings{slif, author = {G. De Micheli}, title = "{Synchronous Logic Synthesis}", booktitle = iwls, address = {North Carolina}, month = may, year = 1989 } %% %% State Assignment %% @inproceedings{jedi, author = {B. Lin and A. R. Newton}, title = "{Synthesis of Multiple Level Logic from Symbolic High-Level Description Languages}", booktitle = vlsi, pages = {187-196}, month = aug, year = 1989 } %% Tiziano says the TransCad reference is the best one for NOVA @article{nova, author = {T. Villa and A. L. Sangiovanni-Vincentelli}, title = "{NOVA: State Assignment of Finite State Machines for Optimal Two-Level Logic Implementations}", journal = ieeetcad, volume = 9, number = 9, pages = {905-924}, month = sep, year = 1990 } @inproceedings{nova-dac, author = {T. Villa and A. L. Sangiovanni-Vincentelli}, title = "{NOVA: State Assignment of Finite State Machines for Optimal Two-Level Logic Implementations}", booktitle = dac, pages = {327-332}, year = 1989 } @inproceedings{shen92, author = {J.-J. Shen and Z. Hasan and M. J. Ciesielski}, title = "{State Assignment for General FSM Networks}", booktitle = iccd, pages = {245-249}, month = oct, year = 1992 } @article{devadas91a, author = {S. Devadas and A. R. Newton}, title = "{Exact Algorithms for Output Encoding, State Assignment and Four-Level Boolean Minimization}", journal = ieeetcad, volume = 10, number = 1, pages = {13-27}, month = jan, year = 1991 } %% %% State Minimization %% @article{paull59, author = {M. C. Paull and S. H. Unger}, title = "{Minimizing the Number of States in Incompletely Specified Sequential Switching Functions}", journal = ire, month = sep, volume = {EC-8}, pages = {356-367}, year = 1959 } @inproceedings{stamina, author = {G. D. Hachtel and J.-K. Rho and F. Somenzi and R. Jacoby}, title = "{Exact and Heuristic Algorithms for the Minimization of Incompletely Specified State Machines}", booktitle = edac, pages = {184-191}, address = {Amsterdam, The Netherlands}, month = feb, year = 1991 } %% %% Technology Mapping %% @phdthesis{touati_thesis, author = {Herv\'{e} J. Touati}, title = "{Performance-Oriented Technology Mapping}", school = ucb, year = 1990, note = {Memorandum No. UCB/ERL M90/109}, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = nov } @inproceedings{wang-iwls-97, author = "Qi Wang and Sarma Vrudhula", title = "{Optimizations for Sequential Circuits Without Global Resets by Structural Transformations}", booktitle = iwls, month = may, year = 1997 } @inproceedings{hojati-iwls-97, author = "R. Hojati and A. Kuehlmann and S. German and R. Brayton", title = "{Validity Checking in the Theory of Equality Using Finite Instantiations}", booktitle = iwls, month = may, year = 1997 } @inproceedings{amit-iwls-97, author = "P. Buch and A. Narayan and R. Newton and A. Sangiovanni-Vincentelli", title = "{Synthesis for Pass-Transistor Logic}", booktitle = iwls, month = may, year = 1997 } @inproceedings{moon89, author = "C. W. Moon and B. Lin and H. Savoj and R. K. Brayton", title = "{Technology Mapping for Sequential Logic Synthesis}", booktitle = iwls, address = {North Carolina}, month = may, year = 1989 } @inproceedings{touati90a, author = {H. Touati and C. Moon and R. K. Brayton and A. Wang}, title = "{Performance-Oriented Technology Mapping}", booktitle = mit6, pages = "79-97", month = apr, year = 1990 } %% %% Testing %% %% Need Memorandum Number: @phdthesis{ghosh_thesis, author = "Abhijit Ghosh", title = "{Techniques for Test Generation and Verification in VLSI Sequential Circuits}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = dec, year = 1991 } @inproceedings{kundu-itc-92, author = {S. Kundu and L. H. Huisman and I. Nair and V. S. Iyengar and L. N. Reddy}, title = "{A Small Test Generator for Large Designs}", booktitle = itc, pages = {30-40}, year = 1992 } @inproceedings{larrabee89, author = {T. Larrabee}, title = "{Efficient Generation of Test Patterns Using Boolean Difference}", booktitle = itc, pages = {795-801}, year = 1989 } %% Path recurrence techniques reference: @inproceedings{mcgeer91, author = {P. McGeer and A. Saldanha and P. Stephan and R. K. Brayton and A. Sangiovanni-Vincentelli}, title = "{Timing Analysis and Delay-Fault Test Generation using Path Recursive Functions}", booktitle = iccad, pages = {180-183}, month = nov, year = 1991 } %% Need Memorandum Number: @phdthesis{saldanha_thesis, author = "Alexander Saldanha", title = "{Performance and Testability Interactions in Logic Synthesis}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = dec, year = 1991 } %% %% Verification %% @techreport{blifmv, author = {R. K. Brayton and M. Chiodo and R. Hojati and T. Kam and K. Kodandapani and R. P. Kurshan and S. Malik and A. L. Sangiovanni-Vincentelli and E. M. Sentovich and T. Shiple and K. J. Singh and H.-Y. Wang}, title = "{BLIF-MV: An Interchange Format for Design Verification and Synthesis}", institution = erl, number = {UCB/ERL M91/97}, address = {Univ. of California, Berkeley, CA 94720}, month = nov, year = 1991 } %% publisher = {Springer-Verlag}, %% address = {Grenoble, France}, @inproceedings{coudert89, author = {O. Coudert and C. Berthet and J. C. Madre}, title = "{Verification of Sequential Machines Based on Symbolic Execution}", booktitle = "{Proc. of the Workshop on Automatic Verification Methods for Finite State Systems}", series = lncs, volume = 407, editor = "{J.~Sifakis}", month = jun, pages = {365-373}, year = 1989 } @InProceedings{BBLS92, author = "{S. Bensalem} and {A. Bouajjani} and {C. Loiseaux} and {J. Sifakis}", title = "{P}roperty {P}reserving {S}imulations", booktitle = "Proceedings of the Fourth Workshop on Computer-Aided Verification", year = "1992", month = jul, key = "BBLS92", } @inproceedings{coudert90, author = "O. Coudert and J. C. Madre", title = "{A Unified Framework for the Formal Verification of Sequential Circuits}", booktitle = iccad, year = 1990, month = nov, pages = {126-129}, } @inproceedings{cho90, author = {H. Cho and G. D. Hachtel and S.-W. Jeong and B. Plessier and E. Schwarz and F. Somenzi}, title = "{ATPG Aspects of FSM Verification}", booktitle = iccad, pages = {134-137}, month = nov, year = 1990 } @inproceedings{coudert-dac-96, author = {O. Coudert}, title = "{On Solving Covering Problems}", booktitle = dac, month = jun, year = 1996 } @inproceedings{coudert-dac-95, author = {O. Coudert}, title = "{New ideas for solving covering problems}", booktitle = dac, month = jun, year = 1995 } @inproceedings{coudert-dac-97, author = {O. Coudert}, title = "{Coloring Real-life Graphs is Easy}", booktitle = dac, month = jun, year = 1997 } @inproceedings{harris-dac-94, author = {I. Harris and A. Orailoglu}, title = "{Microarchitectural Synthesis of VLSI Designs with High Test Concurrency}", booktitle = dac, pages = {206-211}, month = jun, year = 1994 } @inproceedings{jeong91, author = { S.-W. Jeong and B. Plessier and G. D. Hachtel and F. Somenzi}, title = "{Variable Ordering for FSM Traversal}", booktitle = iccad, month = nov, year = 1991, } @inproceedings{plessier91, author = { S.-W. Jeong and B. Plessier and G. D. Hachtel and F. Somenzi}, title = "{Extended BDDs: Trading off Canonicity for Structure in Verification Algorithms}", booktitle = iccad, month = nov, year = 1991, } @article{pixley92, author = {C. Pixley}, title = "{A Theory and Implementation of Sequential Hardware Equivalence}", journal = ieeetcad, volume = 11, number = 12, pages = {1469-1494}, month = dec, year = 1992 } @inproceedings{otten-dac-98, author = {R. Otten and R. Brayton}, title = "{Planning for Performance}", booktitle = dac, month = jun, year = 1998 } @inproceedings{clarke-dac-99, author = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Masahiro Fujita and Yunshan Zhu}, title = "{Symbolic Model Checking Using Sat Procedures Instead of BDDs}", booktitle = dac, year = 1999 } @inproceedings{govind-dac-98, author = {Shankar Govindaraju and David Dill and Alan Hu and Mark Horowitz}, title = "{Approximate Reachability with BDDs using Overlapping Projections}", booktitle = dac, year = 1998 } @inproceedings{ravi-dac-98, author = {K. Ravi and K. McMillan and T. Shiple and F. Somenzi}, title = "{Approximation and Decomposition of Binary Decision Diagrams}", booktitle = dac, year = 1998 } @unpublished{class-cav-98, author = {EE382m Class Fall 1997}, title = "{Examples of Hardware Verification Using VIS}", note = {Submitted to CAV 1998}, year = 1998 } @unpublished{singhal94a, author = {V. Singhal and C. Pixley}, title = "{The Verification Problem for Replaceability}", note = {Submitted for publication}, year = 1994 } @inproceedings{hojati92, author = {R. Hojati and H. Touati and R. P. Kurshan and R. K. Brayton}, title = "{Efficient $\omega$-Regular Language Containment}", booktitle = "{Proc. of the Fourth Workshop on Computer-Aided Verification}", address = {Montr\'{e}al, Qu\'{e}bec, Canada}, pages = "371-382", year = 1992 } @inproceedings{kukimoto-dac-98, author = {Y. Kukimoto and R. K. Brayton and P. Sawkar}, title = "{Delay-optimal technology mapping by DAG mapping}", booktitle = dac, month = jun, year = 1998 } @inproceedings{kukimoto-dac-97, author = {Y. Kukimoto and R. K. Brayton}, title = "{Timing Optimization in the Presence of False Paths}", booktitle = dac, address = {Anaheim, CA}, month = jun, year = 1997 } @inproceedings{hojati93a, author = {R. Hojati and T. R. Shiple and R. K. Brayton and R. P. Kurshan}, title = "{A Unified Environment for Language Containment and Fair CTL Model Checking}", booktitle = dac, address = {Dallas, Texas}, pages = "475-481", month = jun, year = 1993 } @inproceedings{hojati93b, author = {R. Hojati and R. K. Brayton and R. P. Kurshan}, title = "{BDD-Based Debugging of Design Using Language Containment and Fair CTL}", booktitle = "{Proc. of the Conf. on Computer-Aided Verification}", volume = 697, editor = "C. Courcoubetis", publisher = {Springer-Verlag}, pages = "41-58", month = jun, year = 1993 } @techreport{hojati93c, author = {R. Hojati and V. Singhal and R. K. Brayton}, title = "{Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment}", institution = src, number = {SRC Pub C93284}, address = {79 Alexander Dr., Building 4401, Suite 300, P. O. Box 12053, Research Triangle Park, NC 27709}, year = 1993 } @unpublished{hojati94a, author = {R. Hojati and V. Singhal and R. K. Brayton}, title = "{Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment}", note = {Submitted for publication}, year = 1994 } @misc{newblifmv-report, author = {Berkeley CAD group}, title = "{Revisiting BLIF-MV, An Intermediate Format for Verification and Synthesis of Hierarchical Networks of FSMs}", year = 1993 } @inproceedings{balarin93a, author = "F. Balarin and G. York", title = "{Verilog {HDL} Modeling Styles for Formal Verification}", booktitle = "{IFIP Conference on Hardware Description Languages and their Applications}", publisher = {OCRI Publications}, year = 1993, month = apr, pages = {439-452}, annote = {}, keywords = {}, affiliation = {UC Berkeley}, entered = {T. Shiple, 7/8/93}, } @misc{hsis-report, author = {Huey-Yih Wang}, title = "{BLIF-MV and HSIS Data Structure}", month = dec, year = 1992 } @misc{hsis-manual, author = {Berkeley CAD group}, title = "{HSIS Users Manual}", month = sep, year = 1993 } @misc{pif-manual, author = {Berkeley Verifiers}, title = "{PIF: a Property Interchange Format for verification using HSIS}", year = 1993 } @inproceedings{singhal-iccad-98, author = {J. Burch and V. Singhal}, title = "{Tight Integration of Combinational Verification Methods}", booktitle = iccad, year = 1998 } @inproceedings{chiodo92, author = {M. Chiodo and T. R. Shiple and Sangiovanni-Vincentelli, A. L.}, title = "{Automatic Compositional Minimization in CTL Model Checking}", booktitle = iccad, pages = {172-178}, year = 1992 } @techreport{internal-report, title = "{Synthesis for Pass Transistor Logic}", autho = {"Internal Report"} } @Book{schoenfield93, author = "J. R. Schoenfield", title = "Recursion Theory", publisher = "Springer-Verlag", address = "Berlin", year = "1993" } @Book{addison65, author = "J. W. Addison and L. Henkin and A. Tarski", title = "The Theory of Models", publisher = "North-Holland", address = "Amsterdam", year = "1965"} @Book{henkin71, author = "L. Henkin and J. D. Monk and A. Tarski", title = "Cylindric Algebras", publisher = "North-Holland", address = "Amsterdam", year = "1971", ISBN = "0-7204-2043-1" } @inproceedings{andreas-dac-97, author = {Andreas Kuehlmann and Florian Krohm}, title = "{Equivalence Checking Using Cuts and Heaps}", booktitle = dac, month = jun, year = 1997, } @inproceedings{burch91b, author = {J. R. Burch and E. M. Clarke and D. E. Long}, title = "{Representing Circuits More Efficiently in Symbolic Model Checking}", booktitle = dac, month = jun, year = 1991, } @inproceedings{eisner94, author = {Cindi Eisner and Daniel Geist and Ilan Beer and Ranaan Gerwitzmann}, title = "Industrial Strength Formal Verification", booktitle = "{Computer Aided Verification}", series = lncs, volume = 818, publisher = {Springer-Verlag}, year = 1994, } @inproceedings{beer94a, author = {Daniel Geist and Ilan Beer}, title = "Efficient Model Checking by Automated Ordering of Transition Relation Partitions", booktitle = "{Computer Aided Verification}", series = lncs, volume = 818, publisher = {Springer-Verlag}, pages = {52-71}, year = 1994, } @inproceedings{hojat-iccd-97, author = {Shervin Hojat and Paul Villarrubia}, title = "{An Integrated Placement and Synthesis Approach for Timing Closure of PowerPC Microprocessors}", booktitle = iccd, month = oct, year = 1997, } @inproceedings{somenzi94, author = {H. Cho and G. D. Hachtel and E. Macii and M. Poncino and F. Somenzi}, title = "{A Structural Approach to State Space Decomposition for Approximate Reachability Analysis}", booktitle = iccd, month = oct, year = 1994, } @inproceedings{hu94, author = { Alan J. Hu and Gary York and David L. Dill}, title = "{New Techniques for Efficient Verification with Implicitly Conjoined BDDs}", booktitle = dac, pages = {276-282}, month = jun, year = 1994 } @inproceedings{hojati-fmcad-96, author = {R. Hojati and A. Isles and D. Kirkpatrick and R. Brayton}, title = "{Verification Using Finite Instantiations and Uninterpreted Functions}", booktitle = fmcad, month = nov, year = 1996 } @inproceedings{barrett-fmcad-96, author = {C. Barrett and D. Dill and Jeremy Levitt}, title = "{Validity Checking for Combinations of Theories with Equality}", booktitle = fmcad, month = nov, year = 1996 } @inproceedings{mcmillan-cav-94, author = {K. McMillan}, title = "{Hierarchical representations of discrete functions with applications to model checking}", booktitle = cav, month = jul, year = 1994 } @inproceedings{burch-cav-94, author = {J. Burch and D. Dill}, title = "{Automatic Verification of Microprocessor Control}", booktitle = cav, month = jul, year = 1994 } @Book{ack_book, author = "Wilhelm Ackermann", title = "Solvable Cases of the Decision Problem", publisher = "North-Holland", series = "Studies in Logic and the Foundations of Mathematics", address = "Amsterdam", year = "1954", } @inproceedings{singhal-cav-94, author = {V. Singhal and C. Pixley}, title = "{The Verification Problem for Replaceability}", booktitle = cav, month = jul, year = 1994 } @inproceedings{ho95, author = {Pei-Hsin Ho and Howard Wong-Toi}, title = "{ Automated analysis of an audio control protocol}", booktitle = cav, year = 1995 } @inproceedings{emerson93, author = {A. Emerson and E. Sistla}, title = "{Symmetry in Model Checking}", booktitle = cav, month = jun, year = 1993 } @inproceedings{jha93, author = {E. M. Clarke and T. Filkorn and S. Jha}, title = "{Exploiting Symmetries in Temporal Logic Model Checking}", booktitle = cav, month = jun, year = 1995 } @inproceedings{fix94, author = {R. Alur and L. Fix and T.A. Henzinger}, title = "{A Determinizable Class of Timed Automata}", month = jun, booktitle = cav, year = 1994 } @inproceedings{graf94, author = {S. Graf}, title = "{Verification of a Distributed Cache Memory by Using Abstractions}", mon = jun, booktitle = cav, year = 1994 } @article{harkness94, author = { C. Harkness and E. Wolf}, title = "{Verifying the Summit Bus Converter Protocols with Symbolic Model Checking}", journal = "Formal Methods in System Design", month = feb, volume = {4}, Pages = {83-99}, Year = 1994 } @article{gupta92, author = { A. Gupta}, title = "{Formal Hardware Verification Methods: A Survey}", journal = "Formal Methods in System Design", month = oct, volume = {1}, Pages = {151-238}, Year = 1993 } @inproceedings{dill91, author = {D. L. Dill and A. J. Hu and H. Wong-Toi}, title = "{Checking for Language Inclusion Using Simulation Preorder}", booktitle = "{Proc. of the Third Workshop on Computer-Aided Verification}", year = 1991 } @inproceedings{alur90, author = {R. Alur and D. L. Dill}, title = "{Automata for Modeling Real Time Systems}", booktitle = "International Colloquium on Automata, Languages and Programming", year = 1990 } @inproceedings{wong-toi90, author = {H. Wong-Toi and D. L. Dill}, title = "{Synthesizing Processes and Schedulers from Temporal Specifications}", booktitle = "{Proc. of the Second Workshop on Computer-Aided Verification}", year = 1990 } @inproceedings{dill92, author = {D. L. Dill and A. J. Drexler and A. J. Hu and C. H. Yang}, title = "{Protocol Verification as a Hardware Design Aid}", booktitle = iccd, pages = {522-525}, month = oct, year = 1992 } @inproceedings{burch93, author = {J. R. Burch and D. L. Dill and E. Wolf and G. D. Micheli}, title = "{Modeling Hierarchical Combinational Circuits}", booktitle = iccad, pages = {612-617}, month = nov, year = 1993 } @inproceedings{touati90b, author = {H. Touati and H. Savoj and B. Lin and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title = "{Implicit State Enumeration of Finite State Machines using BDDs}", booktitle = iccad, pages = {130-133}, month = nov, year = 1990 } @inproceedings{camurati92, author = { G. Cabodi and P. Camurati and F. Corno and S. Gai and P. Prinetto and M. Sonza Reorda}, title = "{A New Model for Improving Symbolic Product Machine Traversal}", booktitle = dac, pages = {614-619}, month = jun, year = 1992, } @inproceedings{cabodi-iccd-94, author = { G. Cabodi and P. Camurati and S. Quer}, title = "{Efficient State Space Pruning in Symbolic Backward Traversal}", booktitle = iccd, pages = {230-236}, month = oct, year = 1994, } @inproceedings{camurati93, author = { G. Cabodi and P. Camurati}, title = "{Exploiting Cofactoring for Efficient FSM Symbolic Traversal Based on the Transition Relation}", booktitle = iccd, pages = {299-313}, month = oct, year = 1993, } @inproceedings{pixley90a, author = {C. Pixley}, title = "{A Computational Theory and Implementation of Sequential Hardware Equivalence}", booktitle = "{Proc. of the Workshop on Computer-Aided Verification}", editor = "E.~M. Clarke and R.~P. Kurshan", pages = "293-320", month = jun, year = 1990 } @inproceedings{berman89, author = { C.L. Berman}, title = "{Ordered Binary Decision Diagrams and Circuit Structure}", booktitle = iccd, month = oct, year = 1989 } @unpublished{harkness92, author = {H. L. Harkness and G. M. Swamy}, title = "{Minimization of Transition Relation Representations for Complex FSM's}", note = "{EE290H Class Project Report}", month = dec, year = 1992 } @inproceedings{touati90c, author = {H. Touati and R. K. Brayton and R. P. Kurshan}, title = "{Checking Language Containment using BDDs}", booktitle = "{Proc. of Intl. Workshop on Formal Methods in VLSI Design}", address = "{Miami, FL}", month = jan, year = 1990 } @article{burch90, author = {J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill}, title = "{Symbolic Model Checking: $10^{20}$ States and Beyond}", journal = "{Information and Computation}", volume = 98, number = 2, pages = {142-170}, year = 1992 } @article{browne88, author = {M. C. Browne and E. M. Clarke and O. Grumberg}, title = "{Characterizing Finite Kripke Structures in Propositional Temporal Logic}", journal = "{Theoretical Computer Science}", volume = 59, pages = {115-131}, year = 1988 } @article{parrow89, author = {J. Parrow}, title = "{Submodule construction and equation solving in CCS}", journal = "{Theoretical Computer Science}", volume = 68, year = 1989 } @inproceedings{jljl93, author = {O. H. Jensen and J. T. Lang and C. Jeppesen and K. G. Larsen}, title = "Model construction for implicit specifications in modal logic", series = lncs, volume = 715, publisher = {Springer-Verlag}, year = 1993 } @inproceedings{jon91, author = {B. Jonsson and K. G. Larsen}, title = "On the complexity of equation solving in process algebra", booktitle = "{TAPSOFT 1991}", series = lncs, volume = 493, publisher = {Springer-Verlag}, year = 1991 } @article{koller-siam-94, author = {D. Koller and N. Megiddo}, title = "{Constructing small sample spaces satisfying given constraints}", journal = siam_dm, pages = {260-274}, mon = may, year = 1994 } @article{wor87, author = {W. Wonham and P. Ramadge}, title = "{On the supremal controllable language of a given language}", journal = siam_opt, volume = 25, pages = {637-659}, year = 1988 } @article{raw89, author = { P. Ramadge and W. Wonham}, title = "{The control of discrete event systems}", journal = pieee, volume = 77, pages = {81-98}, mon = jan, year = 1989 } @inproceedings{bss94, author = { M. DiBenedetto and A. Saldanha and A. Sangiovanni-Vincentelli}, title = "{Model matching for finite state machines}", booktitle = cdc, month = dec, year = 1994 } @unpublished{tasiran95a, author = {S. Tasiran and R. Hojati and R. K. Brayton}, title = "{Language Containment of Non-Deterministic $\omega$-Automaton}", note = {Submitted for publication}, year = 1995 } @inproceedings{ness93, author = "{E. M. Clarke and O. Grumberg and H. Hiraisi and S. Jha and D. E. Long and K. L. McMillan and L. A. Ness}", title = "{Verification of the Futurebus+ Cache Coherence Protocol}", booktitle = "{Proc. 11th Intl. Symp. on Comput. Hardware Description Lang. and their Applications}", year = 1993 } @unpublished{plessier94, author = {B. Plessier and V. Singhal and C. Pixley}, title = "{Formal Verification as a Hardware Debugger}", note = {To be submitted for publication}, year = 1994 } @inproceedings{mcmillan91, author="K. L. McMillan and J. Schwalbe", title="{Formal Verification of the Encore Gigamax Cache Consistency Protocols}", booktitle="International Symposium on Shared Memory Multiprocessors", year = "1991", month = apr, } @book{mcmillan_thesis, author = "McMillan, K. L.", title = "{Symbolic Model Checking}", publisher = {Kluwer Academic Publishers}, year = 1993 } @book{boyer88, author = {R. S. Boyer and J. S. Moore}, title = "{A Computational Logic Handbook}", year = 1988, address = {New York}, publisher = {Academic Press} } @incollection{gordon88, author = {M. Gordon}, title = "{HOL: A Proof Generating System for Higher-order Logic}", booktitle = "{VLSI Specification, Verification and Synthesis}", year = 1988, pages = {73-127}, editor = {G. Birwistle and P. A. Subrahmanyam}, address = {Boston}, publisher = {Academic Press} } @inproceedings{grumberg91, author = {O. Grumberg and D. E. Long}, title = "{Model Checking and Modular Verification}", series = lncs, booktitle = "{Proc. of CONCUR '91: 2nd Inter. Conf. on Concurrency Theory}", volume = 527, editor = "J. C. M. Baeten and J. F. Groote", publisher = {Springer-Verlag}, month = aug, year = 1991, } @inproceedings{bouajjani90, author = { A. Bouajjani and J.C. Fernandez and N. Halbwachs}, title = "{Minimal Model Generation}", series = lncs, booktitle = "{Proc. of CAV 1990}", volume = 531, editor = "E. Clarke and R. Kurshan", publisher = {Springer-Verlag}, year = 1990, } @article{clarke92, author = {E. M. Clarke and J. R. Burch and O. Grumberg and D. E. Long and K. L. McMillan}, title = "{Automatic Verification of Sequential Circuit Designs}", journal = "{Phil. Trans. of the Royal Society of London}", volume = 339, pages = {105-120}, year = 1992, } @article{grumberg94, author = {O. Grumberg and D. Long}, title = "{ Model checking and modular verification}", journal = toplas, volume = 16, number = 3, pages = {843-871}, year = 1994 } @article{clarke86, author = {E. M. Clarke and E. A. Emerson and A. P. Sistla}, title = "{Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications}", journal = toplas, volume = 8, number = 2, pages = {244-263}, year = 1986 } @inproceedings{clarke81, author = {E. M. Clarke and E. A. Emerson}, title = "{Design and Synthesis of Synchronization Skeletons Using Branching Time Logic}", booktitle = "{Proc. Workshop on Logic of Programs}", series = lncs, volume = 131, publisher = {Springer-Verlag}, pages = {52-71}, year = 1981, } %Allan Borodin, Jon M. Kleinberg, Prabhakar Raghavan, Madhu Sudan, David P. Williamson: Adversarial queuing theory. JACM 48(1): 13-38 (2001) @article{borodin-jacm-01, author = {A. Borodin and J. Kleinberg and P. Raghavan and M. Sudan and D. Williamson}, title = "{Adversarial queuing theory}", journal = jacm, volume = 48, number = 1, pages = {13-38}, year = 2001 } @article{shostak79, author = {R. E. Shostak}, title = "{A practical decision procedure for arithmetic with function symbols}", journal = jacm, volume = 26, number = 2, pages = {351-360}, year = 1979 } @article{emerson86, author = {E. A. Emerson and J. Y. Halpern}, title = "{``Sometimes'' and ``Not Never'' Revisited: on Branching versus Linear Time Temporal Logic}", journal = jacm, volume = 33, number = 1, pages = {151-178}, year = 1986 } @InCollection{handbook-milner, author = "R. Milner", title = "Semantics of Concurrent Processes", booktitle = "Handbook of Theoretical Computer Science", editor = "J. van Leeuwen", publisher = "North Holland", address = "Amsterdam", year = "1989", } @article{manna84, author = {Z. Manna and P. Wolper}, title = "{Synthesis of Communicating Processes from Temporal Logic Specifications}", journal = toplas, volume = 6, number = 1, pages = {68-93}, year = 1984 } @Article{wolper83, author = "P. Wolper", title = "Temporal Logic Can Be More Expressive", journal = "Information and Computation (formerly Information and Control)", volume = "56", year = "1983", } @inproceedings{emerson87, author = {E. A. Emerson and C. L. Lei}, title = "{Modalities for Model Checking: Branching Time Strikes Back}", booktitle = popl, pages = {84-96}, year = 1985 } @inproceedings{pneuli89, author = {A. Pnueli and R. Rosner}, title = "{On the Synthesis of a Reactive Module}", booktitle = popl, pages = {179-190}, year = 1989 } @article{pneuli93, author = {A. Pnueli and L. Zuck}, title = "{Probabilistic verification}", journal = iac, volume = 103, number = 1, pages = {1-29}, year = 1993 } @article{zvi90, author = {Z. Har'El and R. P. Kurshan}, title = "{Software for Analytical Development of Communication Protocols}", journal = att, month = jan, year = 1990, pages = {45-59} } @article{kurshan87a, author = {R. P. Kurshan}, title = "{Complementing Deterministic B\"{u}chi Automata in Polynomial Time}", journal = "Journal of Computer and System Sciences", volume = 35, year = 1987, pages = {59-71} } @incollection{kurshan87b, author = {R. P. Kurshan}, title = "{Reducibility in Analysis of Coordination}", series = "LNCS", volume = 103, year = 1987, booktitle = "Discrete Event Systems: Models and Applications", publisher = {Springer-Verlag}, pages = {19-39} } @incollection{kozen90, author = {D. Kozen and J. Tiuryn}, title = "{Logics of Programs}", booktitle = "Formal Models and Semantics", series = "Handbook of Theoretical Computer Science", volume = "B", year = 1990, pages = {789-835}, editor = {J. van Leeuwen}, publisher = {Elsevier Science} } @incollection{emerson90, author = {E. A. Emerson}, title = "{Temporal and Modal Logic}", booktitle = "Formal Models and Semantics", series = "Handbook of Theoretical Computer Science", volume = "B", year = 1990, pages = {996-1072}, editor = {J. van Leeuwen}, publisher = {Elsevier Science} } @incollection{thomas90, author = {W. Thomas}, title = "{Automata on Infinite Objects}", booktitle = "Formal Models and Semantics", series = "Handbook of Theoretical Computer Science", volume = "B", year = 1990, pages = {133-191}, editor = {J. van Leeuwen}, publisher = {Elsevier Science} } @article{sistla87, author = {A. P. Sistla and M. Y. Vardi and P. L. Wolper}, title = "{The Complementation Problem for B\"{u}chi Automata, with Applications to Temporal Logic}", journal = "Theoretical Computer Science", volume = 49, year = 1987, pages = {217-237} } % for bisimulation @phdthesis{vanglabbeek_thesis, author = "van Glabbeek, R. J.", title = "{Comparative Concurrency Semantics and Refinement of Actions}", school = "{Centrum voor Wiskunde en Informatica, Vrije Universiteit te Amsterdam}", address = {Amsterdam}, month = may, year = 1990 } @article{choueka74, author = {Y. Choueka}, title = "{Theories of Automata on omega-Tapes: A Simplified Approach}", journal = "JCSS", volume = "8(2)", year = 1974, pages = {117-141} } @phdthesis{safra_thesis, author = {S. Safra}, title = "{Complexity of Automata on Infinite Objects}", school = "The Weizmann Institute of Science", address = {Rehovot, Israel}, month = mar, year = 1989 } @phdthesis{long_thesis, author = {David E. Long}, title = "{Model Checking, Abstraction and Compositional Verification}", school = "Carnegie Mellon University ", address = {Pittsburgh, PA}, month = jul, year = 1993 } @inproceedings{safra92, author = {S. Safra}, title = "{Exponential Determinization for $\omega$-Automata with Strong-Fairness Acceptance Condition}", booktitle = stoc, year = 1992 } @inproceedings{necula-lics-98, author = {George C. Necula and Peter Lee}, title = "{Efficient Representation and Validation of Proofs}", booktitle = lics, month = jun, year = 1998 } @inproceedings{clarke89, author = {E. M. Clarke and K. McMillan and D. Long}, title = "{Compositional Model Checking}", booktitle = lics, month = jun, year = 1989 } @inproceedings{vardi86, author = {M. Y. Vardi and P. L. Wolper}, title = "{An Automata-Theoretic Approach to Program Verification}", booktitle = lics, pages = {332-334}, year = 1986 } @book{kurshan93, author = {R. P. Kurshan}, title = "{Automata-Theoretic Verification of Coordinating Processes}", publisher = {Princeton University Press}, year = 1993 } @book{rabin72, author = {M. O. Rabin}, title = "{Automata on Infinite Objects and Church's Problem}", series = "Regional Conf. Series in Mathematics", volume = 13, year = 1972, publisher = {American Mathematical Society}, address = {Providence, Rhode Island}, pages = {19-39} } @incollection{manna81, author = "Z. Manna and A. Pnueli", title = "{Verification of Concurrent Programs: The Temporal Framework}", booktitle = {The Correctness Problem in Computer Science}, editor = "R. S. Boyer and J. S. Moore", series = "Int. Lecture Series in Computer Science", address = "London", publisher = "Academic Press", pages = "215-273", year = 1981, entered = {T. Shiple, 1/25/93}, } @article{streett82, author = {R. S. Streett}, title = "{Propositional Dynamic Logic of Looping and Converse is Elementary Decidable}", journal = "Information and Control", volume = 54, year = 1982, pages = {121-141} } %% %% Concurrency %% @book{milner89, author = "R. Milner", title = "Communication and Concurrency", publisher = "Prentice Hall", address = "New York", year = 1989, affiliation = {Edinburgh} } %% %% Probabilistic Verification %% @inproceedings{emerson-icalp-81, author = {E. A. Emerson and E. M. Clarke}, title = "{Characterizing Correctness Properties of Programs as Fixpoints}", booktitle = icalp, year = 1981 } @inproceedings{cour90, author = {C. Courcoubetis and M. Yannakakis}, title = "{Automatic Verification of Finite State Programs}", booktitle = icalp, pages = {326-347}, year = 1990 } @inproceedings{cleavland92, author = {R. Cleavland and S. A. Smolka and A. Zwarico}, title = "{Testing Preorders for Probabilistic Processes}", booktitle = icalp, pages = {708-719}, year = 1992 } @inproceedings{alur91, author = {R. Alur and C. Courcoubetis and D. Dill}, title = "{Model Checking for Probabilistic Real Time Systems}", booktitle = icalp, pages = {115-126}, year = 1991 } @inproceedings{acd90, author = {R. Alur and C. Courcoubetis and D. Dill}, title = "{Model Checking for Real-Time Systems}", booktitle = lics, pages = {414-425}, year = 1990 } @inproceedings{cour88, author = {C. Courcoubetis and M. Yannakakis}, title = "{Verifying Temporal Properties of Finite State Probabilistic Programs}", booktitle = focs, pages = {338-345}, year = 1988 } @inproceedings{vardi85, author = {M. Y. Vardi}, title = "{Automatic Verification of Finite State Programs}", booktitle = focs, pages = {327-338}, year = 1985 } @inproceedings{hart84a, author = {S. Hart and M. Shamir}, title = "{Probabilistic Temporal Logics for Finite and Bounded Models}", booktitle = stoc, pages = {1-13}, year = 1984 } @inproceedings{ben-or84, author = {M. Ben-Or and D. Kozen and J. Reif}, title = "{The Complexity of Elementary Algebra and Geometry}", booktitle = stoc, pages = {457-464}, year = 1984 } @book{tarski51, author = {A. Tarski}, title = "{A Decision Procedure for Elementary Algebra and Geometry}", publisher = "University of California Press", year = 1951 } @book{niven56, author = {I. Niven}, title = "{Irrational Numbers}", publisher = "John-Wiley", year = 1956 } @book{kailath80, author = {T. Kaliath}, title = "{Linear Systems}", publisher = "Prentice-Hall", year = 1980 } @book{numbers, author = {J. H. Ewing}, title = "{Numbers}", publisher = "Springer-Verlag", year = 1991 } @book{ross83, author = {S. Ross}, title = "{Stochastic Processes}", publisher = "John-Wiley", year = 1983 } @inproceedings{feldman83, author = {Y. A. Feldman}, title = "{A Decidable Propositional Probabilistic Dynamic Logic}", booktitle = stoc, pages = {298-309}, year = 1983 } @inproceedings{proverb_aaai_99, author = {Greg A. Keim and Noam Shazeer and Michael Littman and Sushant Agrawal and Catherine M. Cheves and Joseph Fitzgerald and Jason Grosland and Fan Jiang and Shannon Pollard and Karl Weinmeister}, title = "{{\sc Proverb}: The Probabilistic Cruciverbalist}", booktitle = aaai, year = 1999 } @inproceedings{selman94, author = {Bart Selman and Henry Kautz and Bram Cohen}, title = "{Noise Strategies for Improving Local Search}", booktitle = aaai, pages = {337-343}, year = 1994 } @inproceedings{kozen83, author = {D. Kozen}, title = "{A Probabilistic PDL}", booktitle = stoc, pages = {291-297}, year = 1983 } @inproceedings{feldman82, author = {Y. A. Feldman and D. Harel}, title = "{A Probabilistic Dynamic Logic}", booktitle = stoc, pages = {181-195}, year = 1982 } @inproceedings{burch95, author = { Robert B. Jones and David Dill and Jerry R. Burch}, title = "{Efficient Validity Checking for Processor Validation}", booktitle = iccad, pages = {2-6}, year = 1995 } @inproceedings{pardo-iccad-96, author = {W. Lee and A. Pardo and G. D. Hachtel and J. Jang and A. Pardo and F. Somenzi}, title = "{Tearing Based Automatic Abstraction for CTL Model Checking}", booktitle = iccad, year = 1996 } @inproceedings{bahar93, author = {R. I. Bahar and E. A. Frohm and C. M. Gaona and G. D. Hachtel and E. Macii and A. Pardo and F. Somenzi}, title = "{Algebraic Decision Diagrams and their Applications}", booktitle = iccad, pages = {188-192}, year = 1993 } @article{hart84b, author = {S. Hart and M. Sharir and A. Pnueli}, title = "{Verification of Probabilistic Programs}", journal = "SIAM Journal of Computation", volume = 13, year = 1984, pages = {292-314} } @article{hj94, author = {H. Hansson and B. Jonsson}, title = "{A Logic for Reasoning about Time and Reliability}", journal = "Formal Aspects of Computing", volume = 6, year = 1994, pages = {512-535} } @book{revuz75, author = {D. Revuz}, title = "{Markov Chains}", publisher = "North-Holland", year = 1975 } @book{paz71, author = {A. Paz}, title = "{Introduction to Probabilistic Automata}", publisher = "Academic-Press", year = 1971 } @Book{Papa94, author = "Christos H. Papadimitriou", title = "Computational Complexity", publisher = "Addison-Wesley", year = "1994", pages = "523", } P. K. Agarwal and J. Erickson. Geometric range searching and its relatives . In B. Chazelle, J. E. Goodman, and R. Pollack, editors, Advances in Discrete and Computational Geometry, volume 223 of Contemporary Mathematics, pages 1--56. American Mathematical Society, Providence, RI, 1999. @InBook{agarwal_survey, author = {P. K. Agarwal and J. Erickson}, chapter = "Geometric range searching and its relatives", title = "Advances in Discrete and Computational Geometry", publisher = "American Mathematical Society", year = "1999", pages = "1--56", } @InBook{rabin_survey, author = "M. O. Rabin", chapter = "Decidable Theories", note = "{\em ed. by} J. Barwise", title = "Handbook of Mathematical Logic", publisher = "North-Holland", year = "1977", pages = "595--629", } @phdthesis{emiris_thesis, author = {Ioannis Emiris}, title = "{Sparse Elimination and Applications in Kinematics}", school = "University of California at Berkeley", address = {Berkeley, CA}, month = dec, year = 1994 } @phdthesis{rege_thesis, author = {Ashutosh Rege}, title = "{A Toolkit for Algebra and Geometry}", school = "University of California at Berkeley", address = {Berkeley, CA}, month = jun, year = 1996 } %% %% CS Theory %% @book{ahuja-book, author = {Ravindra K. Ahuja and Thomas L. Magnanti and James B. Orlin}, title = "{Network Flows: Theory, Algorithms, and Applications}", publisher = "Prentice Hall", year = 1993 } @book{clr90, author = {T. H. Cormen and C. E. Leiserson and R. H. Rivest}, title = "{Introduction to Algorithms}", publisher = "MIT Press", year = 1989 } @techreport{stockmeyer74, author = {L. J. Stockmeyer}, title = "{The Complexity of Decision Problems in Automata Theory and Logic}", institution = "MIT, Cambridge MA", number = {MAC TR-133}, address = {Project MAC}, year = 1974 } @book{ai_book, author = {P. Jackson}, title = "{Introduction to Artificial Intelligence}", publisher = "Dover", year = 1985 } @book{armstrong_book, author = {M. A. Armstrong}, title = "{Groups and Symmetry}", publisher = "Springer-Verlag", year = 1989 } @book{motwani_book, author = {R. Motwani and P. Raghavan}, title = "{Randomized Algorithms}", publisher = "Cambridge University Press", year = 1995 } @book{bondy-book, author = {J. A. Bondy and U. S. R. Murty}, title = "{Graph Theory With Applications}", publisher = "American-Elsevier", year = 1977 } @book{jaja_book, author = {J. F. JaJa}, title = "{An Introduction to Parallel Algorithms}", publisher = "Addison-Wesley", year = 1992 } @book{leighton_book, author = {F. T. Leighton}, title = "{Introduction to Parallel Algorithms and Architectures: Arrays, Trees, Hypercubes}", publisher = "Morgan-Kaufmann", year = 1991 } @book{hopcroft79, author = {J. Hopcroft and J. Ullman}, title = "{Introduction to Automata Theory, Languages and Computation}", publisher = "Addison-Wesley", year = 1979 } @book{abramovici90, author = {M. Abramovici and M. A. Breuer and A. D. Friedman}, title = "{Digital System Testing and Testable Design}", publisher = "{IEEE Press}", year = 1990 } @book{garey79, author = {M. R. Garey and D. S. Johnson}, title = "{Computers and Intractability}", publisher = "{W. H. Freeman and Co.}", year = 1979 } @book{shuvra96, author = {S. S. Bhattacharyya and P. K. Murthy and E. A. Lee}, title = "{Software Synthesis from Dataflow Graphs}", publisher = "{Kluwer Academic Press}", year = 1996 } @book{attiya-book, author = {H. Attiya and J. Welch}, title = "{Distributed Computing: Fundamentals, Simulations and Advanced Topics}", publisher = "{McGraw Hill}", year = 1998 } @book{keshav-book, author = {S. Keshav}, title = "{An Engineering Approach to Computer Networking}", publisher = "{Addison-Wesley}", year = 1997 } @book{enderton72, author = {H. Enderton}, title = "{A Mathematical Introduction to Logic}", publisher = "{Academic Press}", year = 1972 } @book{vaught_book, author = {R. Vaught}, title = "{Set Theory}", publisher = "{Birkhauser}", year = 1995 } @Book{handbook-logic, editor = "Jon Barwise", title = "Handbook of Mathematical Logic", publisher = "North-Holland", address = "Amsterdam", edition = "second", year = "1978", } @Book{manna-pneuli-book, author = {Z. Manna and A. Pnueli}, title = "{The Temporal Logic of Reactive and Concurrent Systems}", publisher = "Springer-Verlag", year = 1992 } @book{royden88, author = {H. L. Royden}, title = "{Real Analysis}", publisher = "{Macmillan Publishing}", year = 1989 } @book{will_thesis, author = {W. Lam and R. K. Brayton}, title = "{Timed Boolean Functions -- A Unified Framework for Exact Timing Analysis}", publisher = {Kluwer Academic Publishers}, year = 1994 } @phdthesis{stemm-thesis, author = {Mark Stemm}, title = "{A Network Measurement Architecture for Adaptive Applications}", school = ucb, year = 1999 } @phdthesis{shiple_thesis, author = {T. R. Shiple}, title = "{Formal Analysis of Synchronous Hardware}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, year = 1996 } @phdthesis{felice_thesis, author = {Felice Balarin}, title = "{Iterative Methods for Formal Verification of Digital Systems}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, year = 1995 } @phdthesis{arlindo_thesis, author = {A. Oliveira}, title = "{Inductive Learning by Selection of Minimal Complexity Representations.}", school = ucb, year = 1994 } @phdthesis{vigyan_thesis, author = {V. Singhal}, title = "{Design Replacements for Sequential Circuits}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, year = 1996 } @phdthesis{kam_thesis, author = {T. Kam}, title = "{State Minimization of Finite State Machines using Implicit Techniques}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = may, year = 1995 } @mastersthesis{stcheng_thesis, author = {Szu Tsung Cheng}, title = "{Compiling Verilog into Automata}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, number = "UCB/ERL M94/37", year = 1994 } @phdthesis{villa_thesis, author = {Tiziano Villa}, title = "{Encoding Problems in Logic Synthesis}", school = ucb, address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = may, year = 1995 } @phdthesis{alur_thesis, author = {Rajeev Alur}, title = "{Techniques for Automatic Verification of Real-Time Systems}", school = stanford, address = {Department of Computer Sciences, Stanford University}, month = aug, year = 1991 } @phdthesis{charbon-thesis, author = {Edoardo Charbon}, title = "{Constraint-Driven Analysis and Synthesis of High-Performance Analog IC Layout}", school = ucb, address = { University of California at Berkeley}, month = dec, year = 1995 } @InProceedings{meyer72, author = "A. R. Meyer and L. J. Stockmeyer", title = "The equivalence problem for regular expressions with squaring requires exponential space", booktitle = "Proc.\ 13th IEEE Symposium on Foundations of Computer Science (FOCS)", year = "1972", pages = "125--129", } @inproceedings{balarin-cav-93, author = {F. Balarin and A. Sangiovanni-Vincentelli}, title = "{An Iterative Approach to Language Containment}", booktitle = cav, month = aug, year = 1993 } @inproceedings{holzmann-cav-96, author = {G. Holzmann and D. Peled}, title = "{The State of {\sf SPIN}}", booktitle = cav, month = aug, year = 1996 } @inproceedings{dams93, author = {D. Dams and O. Grumberg and R. Gerth}, title = "{Generation of reduced models for fragments of CTL}", booktitle = cav, month = jun, year = 1993 } @inproceedings{ok96, author = {O. Kupferman and M. Vardi}, title = "{Verification of Fair Transition Systems}", booktitle = cav, month = jul, year = 1996 } @inproceedings{campos-cav-96, author = {S. Campos and O. Grumberg}, title = "{Selective Quantitative Analysis and Interval Model Checking}", booktitle = cav, month = jul, year = 1996 } @inproceedings{clarke89a, author = "Edmund M. Clarke and David E. Long and Kenneth L. McMillan", title = "Compositional Model Checking", booktitle = "4th Annual Symposium on Logic in Computer Science", address = {Asilomar, CA}, month = jun, year = 1989, } @misc{rina-personal, author = {R. Panigrahy}, title = "{Cisco Systems}", howpublished = "{Personal communication}", year = 2002 } @misc{kurshan-personal, author = {R. Kurshan}, howpublished = "{Personal communication}", year = 1997 } @misc{yuan-personal, author = {Jun Yuan}, howpublished = "{Personal communication}", year = 1997 } @misc{bob-personal, author = {R. Brayton}, howpublished = "{Personal communication}", year = 1996 } @misc{vigyan-personal-97, author = {Vigyan Singhal}, title = "{Cadence Berkeley Labs}", howpublished = "{Personal communication}", year = 1997 } @article{stephan-tcad-96, author = {Paul Stephan and Robert Brayton and Alberto Sangiovanni-Vincentelli}, title = "{Combinational Test Pattern Generation Using Satisfiability}", journal = ieeetcad, volume = 15, number = 9, year = 1996 } @article{brewer-tcad-96, author = {Ivan Radivojevic and Forrest Brewer}, title = "{A New Symbolic Technique for Control-Dependent Scheduling}", journal = ieeetcad, pages = {45-57}, volume = 15, number = 1, year = 1996 } @inproceedings{kam94, author = {T. Kam and T. Villa and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{A Fully Implicit Algorithm for Exact State Minimization}", booktitle = dac, pages = {684-690}, address = {San Diego, CA}, month = jun, year = 1994 } } @article{demicheli91, author = {De Micheli, G.}, title = "{Synchronous Logic Synthesis: Algorithms for Cycle-Time Minimization}", journal = ieeetcad, month = jan, volume = 10, pages = {63-73}, number = 1, year = 1991 } @book{katz_book, author = {Randy Katz}, title = "{Contemporary logic design}", publisher = "{Benjamin/Cummings Pub. Co.}", year = 1993 } @book{rabaey_book, author = {Jan Rabaey}, title = "{Digital Integrated Circuits: A Design Perspective}", publisher = "{Prentice Hall}", year = 1996 } @book{demicheli_book, author = {G. De Micheli}, title = "{Synthesis and Optimization of Digital Circuits}", publisher = "{McGraw Hill}", year = 1994 } @article{malik94, author = "S.~Malik", title = "{Analysis of Cyclic Combinational Circuits}", journal = ieeetcad, volume = "13", number = 7, pages = {950-956}, month = jul, year = 1994 } @inproceedings{shiple95, author = {T.~R. Shiple and V. Singhal and R.~K. Brayton and A.~L. Sangiovanni-Vincentelli}, title = "{Analysis of Combinational Cycles in Sequential Circuits}", booktitle = iscas, month = may, address = {Atlanta, GA}, year = 1996 } @Book{monk_book, author = "J. D. Monk", year = "1976", publisher = springer, title = "Mathematical Logic", } @Book{nilsson_book, author = "Nils J. Nilsson", year = "1998", publisher = "Morgan-Kaufmann", title = "Artificial Intelligence: A New Synthesis", } @Book{hp_book, author = "John Hennessy and David Patterson and David Goldberg", year = "2002", publisher = "Morgan-Kaufmann", edition = "third", title = "Computer Architecture: A Quantitative Approach", } @Book{weste05, author = "N. H. E. Weste and D. Harris", year = "2005", publisher = "Addison-Wesley", title = "CMOS VLSI Design: A Circuits and Systems Perspective", } @Book{weste_book, author = "N. H. E. Weste and K. Eshragian", year = "1993", publisher = "Addison-Wesley", title = "Principles of CMOS VLSI Design", } @Book{munkres, author = "J. R. Munkres", year = "1974", publisher = "Prentice-Hall", title = "Topology: A first course", } @Book{gray_meyer, author = "P. Gray and P. Hurst and S. Hurst and R. Meyer", year = "2001", publisher = "John-Wiley", title = "Analysis and Design of Analog Integrated Circuits", } @Book{noc_book, author = "H. Tenhunen and A. Jantsch", year = "2003", publisher = "Kluwer Academic Publisher", title = "Networks on Chip", } @Book{lee_book, author = "T. Lee", year = "1998", publisher = "Cambridge University Press", title = "The Design of CMOS Radio-Frequency Integrated Circuits", } } @Book{tarski_truth, author = "A. Tarski", year = "1965", publisher = "Oxford University Press", title = "Introduction to Logic and to the Methodology of Deductive Sciences", } @Book{mead_book, author = "C. Mead and L. Conway", year = "1980", publisher = "Addison-Wesley", title = "An Introduction to VLSI Systems", } @article{srivas90, author = {Mandayam Srivas and Mark Bickford}, title = "Formal Verification of a Pipelined Microprocessor", journal = "IEEE Software", volume = "7", number = 5, pages = {52-64}, month = sep, year = 1990 } @misc{liu-binary, author = "Yi-Yu Liu and Kuo-Hua Wang and TingTing Hwang and C. L. Liu", title = "Binary Decision Diagram with Minimum Expected Path Length", url = "citeseer.nj.nec.com/569343.html" } @article{friedman90, author = {Steven J. Friedman and Kenneth J. Supowit}, title = "Finding the Optimal Variable Ordering for Binary Decision Diagrams", journal = tc, volume = "39", number = 5, pages = {710-713}, month = may, year = 1990 } @InProceedings{KolaitisV92, title = "Fixpoint Logic vs.\ Infinitary Logic in Finite-Model Theory", author = "Phokion G. Kolaitis and Moshe Y. Vardi", pages = "46--57", booktitle = "Proceedings, Seventh Annual {IEEE} Symposium on Logic in Computer Science", year = "1992", month = "22--25 " # jun, address = "Santa Cruz, California", organization = "IEEE Computer Society Press", crossrefonly = "1", comment = "IEEE Computer Society Order Number 2735; Library of Congress Number 91-78307; IEEE Catalog Number 92CH3127-8; ISBN 0-8186-2735-2", } @Article{davis62, author = {M. Davis and G. Logemann and D. Loveland}, title = "A machine program for theorem proving", journal = cacm, number = "5", pages = "394--397", year = "1962" } @Article{davis60, author = {M. Davis and H. Putnam}, title = "A computing procedure for quantifer theory", journal = cacm, number = "7", pages = "201--215", year = "1960" } @Article{manna71, author = "Z. Manna and J. Waldinger", title = "Toward automatic program synthesis", journal = cacm, volume = "14", number = "3", pages = "151--165", month = mar, year = "1971", } @Article{bryant_survey, author = "Randal E. Bryant", title = "Symbolic {Boolean} Manipulation with Ordered Binary-Decision Diagrams", journal = "ACM Computing Surveys", volume = "24", number = "3", pages = "293--318", month = sep, year = "1992", coden = "CMSVAN", ISSN = "0360-0300", bibdate = "Sun Sep 25 10:21:25 1994", url = "http://www.acm.org/pubs/toc/Abstracts/0360-0300/136043.html", } @article{pradhan94, author = "W. Kunz and D. Pradhan", title = "Recursive Learning: A Precise Implication Procedure and its application to Test Verification and and Optimization", journal = ieeetcad, month = sep, year = "1994", } @article{thompson86, author = "K. Thompson", title = "Retrograde Analysis of Certain Endgames.", journal = "ICCA Journal", volume = "9", number = "3", pages = "131--139", year = "1986", } @InProceedings{blum88, title={On a Theory of Computation over the Real Numbers; {NP} Completeness, Recursive Functions and Universal Machines (Extended Abstract)}, author={Blum, Lenore and Shub, Mike and Smale, Steve}, pages={387--397}, crossref={FOCS29}, source={http://theory.lcs.mit.edu/~dmjones/FOCS/focs.bib} } @Proceedings{FOCS29, title={29th Annual Symposium on Foundations of Computer Science}, booktitle={29th Annual Symposium on Foundations of Computer Science}, month={24--26} # oct, year=1988, address={White Plains, New York}, organization={IEEE}, crossrefonly=1, source={http://theory.lcs.mit.edu/~dmjones/FOCS/focs.bib} } @article{booledozer-ibmj-96, author = {L. Stok}, title = "{BooleDozer: Logic Synthesis for ASICs}", journal = "{IBM J. Res. and Devep.}", year = 1996, month = jul, pages = {407-430} } @inproceedings{appenzeller-iccd-95, author = {Appenzeller, D.~P. and Kuehlmann, A.}, title = "{Formal Verification of a PowerPC Microprocessor}", booktitle = iccd, month = oct, address = {Austin, TX}, pages = {79-84}, year = 1995 } @inproceedings{huang96, author = {S.-Y. Huang and K.-T. Cheng and K.-C. Chen and U. Glaeser}, title = "{An ATPG-Based Framework for Verifying Sequential Equivalence}", booktitle = "Proc. Intl. Test Conf.", year = 1996 } @article{cheng93, author = {K.-T. Cheng}, title = "{Redundancy Removal for Sequential Circuits Without Reset States}", journal = ieeetcad, volume = 12, number = 1, pages = {13-24}, month = jan, year = 1993 } @misc{www-wsat, author = {Bart Selman}, howpublished = "{\verb+ftp://ftp.research.att.com/dist/ai/+}" } @misc{www-vis, author = {UC Berkeley}, howpublished = "{\verb+www.cad.eecs.berkeley.edu/~vis+}" } @misc{www-proof-size, author = {Paul Beame}, title = "{Propositional Proof Complexity: Past, Present, and Future}", howpublished = "{\verb+http://www.cs.washington.edu/homes/beame/myversion.ps+}" } @misc{www-sr-practice, howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/publications/SR-practice-99.ps+}" } @misc{www-hppd-class, author = {A. Aziz}, howpublished = "{\verb+http://www.ece.utexas.edu/~alpert/syllabus.html+}" } @misc{www-webcaching, author = {A. Aziz}, howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/web-caching+}" } @misc{adnan_www, author = {A. Aziz}, howpublished = "{\tt http://www.ece.utexas.edu/~adnan/}" } @misc{www-core-seq, author = {A. Aziz}, year = {2000}, howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/publications/www-core-seq.ps+}" } @misc{www-sr-theory, howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/publications/SR-theory-99.ps+}" } @misc{www-nsf-matching, author = {NSF}, howpublished = "{\verb+http://www.nsf.gov/pubs/stis1995/nsf95109/nsf95109.txt+}" } @misc{www-zero-in, author = {Inc., 0-in}, howpublished = "{\tt www.0in.com}" } @misc{www-akamai, author = {Inc., Akamai}, howpublished = "{\tt www.akamai.com}" } @misc{www-synopsys, author = {Inc., Synopsys}, howpublished = "{\tt www.synopsys.com}" } @misc{vsi_proposal, author = {VSI Alliance}, title = "{Virtual Socket Interface Proposal 1.0}", howpublished = "{\tt http://www.vsi.org/}", month = sep, year = 1996 } @article{jephson69, author = {J. S. Jephson and R. P. McQuarrie and R. E. Vogelsberg}, title = "{A Three-Value Computer Design Verification System}", journal = "{IBM J. Res. and Devep.}", year = 1969, vol = 8, pages = {178-188} } @inproceedings{cheng92, author = {K.-T. Cheng and H.-K. T. Ma}, title = "{On the Over-Specification Problem in Sequential ATPG Algorithms}", booktitle = dac, address = {Anaheim, CA}, pages = {16-21}, month = jun, year = 1992 } @inproceedings{mazur88, author = {A. Mazurkiewicz}, title = "{Basic Notions of Trace Theory}", booktitle = "{Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency}", series = lncs, volume = 354, publisher = {Springer-Verlag}, pages = {285-363}, year = 1988 } @inproceedings{peled93, author = {D. Peled}, title = "{All from One, One for All: On Model Checking Using Representatives}", booktitle = "{Proc. of 5th International Conference on Computer Aided Verification}", series = lncs, volume = 697, publisher = {Springer-Verlag}, pages = {409-423}, year = 1993 } %% Tai's references on Pass Transistor Logic @article{neves96, author = {J. L. Neves}, title = "{Maximizing Speed Performance of Multi-Level Combinational Circuits Implemented with Pass Transistor}", booktitle = asic, month = nov, year = 1996, pages = {15-18} } @article{wu85, author = {M. Y. Wu and W. Shu and S. P. Chan}, title = "{A Unified Theory for PS Circuit Design-Switching Network Logic}", journal = "{Int. J. Electron.}", volume = 58, pages = {1-33}, year = 1985 } @article{wu89, author = {M. Y. Wu and I. N. Hajj}, title = "{Switching Network Logic Approach to Sequential MOS Circuit Design}", journal = ieeetcad, volume = 8, pages = {782-794}, year = 1989 } @article{yano90, author = {K. Yano and T. Yamnaka and T. Nishida and M. Satio and K. Shimohigashi and A. Shimizu}, title = "{A 3.8-ns CMOS 16$\times$16-b Multiplier Using Complementary Pass-Transistor Logic}", journal = jssc, volume = 25, number = 2, pages = {388-395}, month = apr, year = 1990 } @article{lai93, author = {F. S. Lai and W. Hwang}, title = "{Differential Cascode Voltage Switch with Pass-Gate (DCVSPG) Logic Tree for High Performance CMOS Digital Systems}", journal = vlsitsa, pages = {358-362}, year = 1993 } @article{parameswar94, author = {A. Parameswar and H. Hara and T. Sakurai}, title = "{A High Speed, Low Power, Swing Restored Pass-Transistor Logic Based Multiply and Accumulate Circuit for Multimedia Applications}", journal = cicc, pages = {278-281}, month = may, year = 1994 } @article{cheung96, author = {T. S. Sheungm and K. Asada}, title = "{Regenerative Pass-Transistor Logic: A Circuit Technique for High Speed Digital Design}", journal = ieicete, volume = {E79-C}, number = 9, pages = {1274-1283}, month = sep, year = 1996 } @article{rubenstein83, author = {J. Rubenstein and P. Penfield and M. A. Horowitz}, title = "{Signal Delay in RC networks}", journal = ieeetcad, volume = {CAD-2}, pages = {202-211}, month = jul, year = 1983 } @phdthesis{horowitz_thesis, author = {M. Horowitz}, title = "{Timing Models for MOS circuits}", school = stanford, address = {Center for Integrated Systems}, year = 1983, } @article{kuroda95, author = {T. Kuroda and T. Sakurai}, title = "{Overview of Low-Power ULSI Circuit Techniques}", journal = ieicete, volume = {E78-C}, number = 4, pages = {334-343}, month = apr, year = 1995 } @inproceedings{iyer-dac-96, author = {M. A. Iyer and D. E. Long and M. Abramovici}, title = "{Identifying Sequential Redundancies Without Search}", booktitle = dac, month = jun, year = 1996 } @inproceedings{thakur-dac-96, author = {S. Thakur and Martin D. F. Wong and S. Hrishnamoorthy}, title = "{Delay Minimal Decomposition of Multiplexers in Technology Mapping}", booktitle = dac, month = jun, address = {Las Vegas, NV}, year = 1996 } @article{gwennap96, author = {Linley Gwennap}, title = "{Digital's 21164 Reaches 500 MHz}", journal = "{Microprocessor Report}", volume = 10, number = 9, month = jul, year = 1996 } @misc{dec96, author = {Digital Equipment Corporation}, title = "{Digital Semiconductor Alpha 21164 Microprocessor Product Brief}", howpublished = "{\tt http://ftp.digital.com/pub/Digital/info/semiconductor/literature/dsc-library.html}", month = sep, year = 1996 } % [SED:peters:92a] % Robert L. Peters. % Getting What You Came For: The Smart Student's Guide to Earning a Master's or a Ph.D. % Noonday Press, 1992. @inproceedings{minato-90, author = {S. Minato and N. Ishiura and S. Yajima}, title = "{Shared binary decision diagram with attribute edges for efficient Boolean function manipulation}", booktitle = dac, month = jun, year = 1990 } @article{yamashita97, author = {S. Yamashita and K. Yano and Y. Sasaki and Y. Akita and H. Chikata and K. Rikino and K. Seki}, title = "{Pass-Transistor/CMOS Collaborated Logic: The Best of Both Worlds}", journal = "{Symposium on VLSI Circuits}", pages = {31-32}, year = 1997 } @article{kunz-iccad-93, author = {W. Kunz}, title = "{HANNIBAL: An Efficient Tool for Logic Verification Based on Recursive Learning}", journal = iccad, year = 1993 } @article{burch91, author = {J.R. Burch and D.E. Long}, title = "{Efficient Boolean Function Matching}", journal = iccad, pages = {408-411}, year = 1991 } @Book{LGWIRE, author = {}, year = "1994", publisher = "{IBM internal publication}", title = "{LGWIRE Users guide}", key = "I" } @Book{QPLACE, author = {}, year = "1994", publisher = "{IBM internal publication}", title = "{QPLACE Users guide}", key = "I" } @misc{atm, title = "{On the Verification and Reimplementation of ATM switch using VIS.}", howpublished = "{\verb+http://www.ece.concordia.ca/~jianping/TR97.html+.}" } @misc{texas97-bench, title = "{Examples~of~HW~Verification~using~VIS.}", howpublished = "{\tt http://godel.ece.utexas.edu/texas97-benchmarks.}" } @Book{discipline-programming, author = "Edsger~W. Dijkstra", year = "1976", publisher = "Prentice-Hall", title = "A Discipline of Programming", } @misc{ueda-www, author = {Kuzunori Ueda}, title = "{\verb+http://www.ueda.info.waseda.ac.jp/~ueda/+}" } @misc{www-tai-map-iccad-99, author = {Tai-Hung Liu}, howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/publications/tai-map.ps+}" } @misc{www-jacome-dac-98, author = {Gustavo deVeciana and Margarida F. Jacome and Jian-Huei Guo}, title = {Hierarchical Algorithms for Assessing Probabilistic Constraints on System Performance}, howpublished = "{\verb+http://horizon.ece.utexas.edu/~jacome/Publications/Welcome.html+}" } @misc{chuck-code-www, author = {Charles Alpert}, title = "{\verb+http://vlsicad.cs.ucla.edu/~cheese/codes.html+}" } @misc{chuck-survey-www, author = {Charles Alpert}, title = "{\verb+http://vlsicad.cs.ucla.edu/~cheese/survey.html+}" } @misc{malik-stat-www, author = { S. Devadas and H-F. Jyu and K. Keutzer and S. Malik}, title = {Statistical timing analysis of combinational logic circuits}, howpublished = "{\verb+http://www.ee.princeton.edu/~sharad/pubs.html+}" } @inproceedings{pedram_dac_91, author = {Massoud Pedram and Narasimha Bhat}, title = "{Layout Driven Technology Mapping}", booktitle = dac, year = 1991, pages = {99-105} } @inproceedings{eaglesham_dac_99, author = {Douglas Eaglesham}, title = "{0.18 micron CMOS and beyond}", booktitle = dac, year = 1999, } @inproceedings{lou_dac_98, author = {Amir H. Salak and Jinan Lou and Massoud Pedram}, title = "{A DSM design flow: putting floorplanning, technology mapping and gate placement together}", booktitle = dac, year = 1998, } @inproceedings{lou_iccad_97, author = {Jinan Lou and Amir H. Salek and Massoud Pedram}, title = "{An Exact Solution to Simultaneous Technology Mapping and Linear Placement Problem}", booktitle = iccad, year = 1997, pages = {671-675} } @inproceedings{sylvester_iccad_98, author = {Dennis Sylvester and Kurt Keutzer}, title = "{Getting to the Bottom of Deep Submicron}", booktitle = iccad, year = 1998, } @inproceedings{hajj_iccad_94, author = {Weitong Chuang and Ibrahim N. Hajj}, title = "{Delay and Area Optimization for Compact Placement by Gate Resizing and Relocation}", booktitle = iccad, year = 1994, } @inproceedings{alpert_dac_97, author = {Chuch Alpert and Anirudh Devgan}, title = "{Wire Segmenting for Improved Buffer Insertion}", booktitle = dac, year = 1997, pages = {588-589} } @article{ee-times-merced, author = {Alexander Wolfe}, title = "{Merced grips Intel in verification vise}", journal = "{EE Times}", year = 1998, volume = "{http://www.eetimes.com/news/98/991news/merced.html}" } @article{ee-times-dsm, author = {Richard Goering}, title = "{Turmoil hits chip design}", journal = "{EE Times}", year = 1999, month = may, volume = 1059 } @article{src-dsm, author = {Semiconductor Research Corporation}, title = "{Top ten problem in synthesis}", journal = "{\verb+http://www.src.org/areas/cadts/synthes.dgw+}", year = 1998, month = dec } @article{pentium-fdiv, author = {T. Coe}, title = "{Inside the Pentium FDIV Bug}", journal = "{Dr.~Dobbs Journal}", year = 1996, month = apr } @article{ee-times-rajeev, author = {Rajeev Madhavan}, title = "{No quick fix for physical design}", journal = "{EE Times}", year = 1999, month = jan, volume = 1045 } @misc{sia-97, author = {Semiconductor Industry Association}, howpublished = "{National technology roadmap for semiconductors}", year = 1997 } @inproceedings{young-iccad-98, author = {F. Y. Young and Martin D. F. Wong}, title = "{Slicing Floorplans with Preplaced Modules}", booktitle = iccad, month = nov, year = 1998, } @inproceedings{brand95, author = {D. Brand and R. A. Bergamaschi and L. Stok}, title = "{Be Careful with Don't Cares}", booktitle = iccad, month = nov, year = 1995, } @inproceedings{qadeer-iccd-96, author = {S. Qadeer and V. Singhal and C. Pixley and R. K. Brayton}, title = "{Latch Redundancy Removal without Global Reset}", booktitle = iccd, month = oct, year = 1996, } @inproceedings{mcleod_dac_99, author = {Jonah McLeod}, title = "{Functional Verification - Real Users, Real Problems, Real Opportunities}", booktitle = dac, year = 1999, } @Article{richardson-zero, author = "Daniel Richardson", title = "How to Recognize Zero", journal = "Journal of Symbolic Computation", volume = "24", number = "6", month = dec, year = "1997" } @inproceedings{pnueli-cav-99, author = {A. Pnueli and Y. Rodeh and O. Shtrichman and M. Siegel}, title = "{Deciding Equality Formulas by Small-Domains Instantiations}", booktitle = cav, month = jul, year = 1999 } @inproceedings{velev-cav-00, author = {R. Bryant and M. Velev}, title = "{Boolean Satisfiability with Transitivity Constraints}", booktitle = cav, month = jul, year = 2000 } @inproceedings{velev-cav-99, author = {R. Bryant and S. German and M. Velev}, title = "{Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions}", booktitle = cav, month = jul, year = 1999 } @inproceedings{velev-dac-99, author = {M. Velev and R. Bryant}, title = "{Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors}", booktitle = dac, month = jun, year = 1999 } @InBook{hopcroft-state-min, author = {J. Hopcroft}, chapter = "{An $n \cdot \log n$ algorithm for minimizing state in a finite automaton}", note = "{\em ed. by} Z. Kohavi and A. Paz", title = "Theory of Machines and Computability", publisher = "Academic Press", year = "1971", } @inproceedings{necula-osdi-96, author = {George C. Necula and Peter Lee}, title = "{Safe Kernel Extensions Without Run-Time Checking}", booktitle = osdi, month = oct, year = 1996 } @inproceedings{karger-stoc-97, author = {David Karger and Eric Lehman and Tom Leighton and Matthew Levine and Daniel Lewin and Rina Panigrahy}, title = "{Consistent Hashing and Random Trees: Distributed Caching Protocols for Relieving Hotspots on the World Wide Web}", booktitle = stoc, month = may, year = 1997 } @inproceedings{harchol-podc-99, author = {Mor Harchol-Balter and Tom Leighton and Daniel Lewin}, title = "{Resource Discovery in Distributed Networks}", booktitle = podc, month = may, year = 1999 } @inproceedings{lee-sops-97, author = {Chandramohan A. Thekkath and Timothy Mann and Edward K. Lee}, title = "{Frangipani: A Scalable Distributed File System}", booktitle = sops, month = oct, year = 1997 } @misc{internet-flooding, author = {John Moy}, title = "{RFC 1583}", howpublished = "{\tt http://www.dsi.unive.it/Connected/RFC/1583}", year = 1994 } @inproceedings{gatech-internet, author = {Ellen W. Zegura and Ken Calvert and S. Bhattacharjee}, title = "{How to Model an Internetwork}", booktitle = infocom, year = 1996, howpublished = "{\tt http://www.cc.gatech.edu/projects/gtitm/}", } @article{stok96, author = {G. Even and I. Spillinger and L. Stok}, title = " Retiming Revisited and Reversed", journal = ieeetcad, volume = "15", number = 3, month = mar, year = 1996, } @inproceedings{dey92, author = {S. Dey and M. Potkonjak and S. Rothweiler}, title = "{Performance Optimization of Sequential Circuits by Eliminating Retiming Bottlenecks}", booktitle = dac, month = jun, year = 1992 } @inproceedings{hassoun96, author = {S. Hassoun and C. Ebeling}, title = "{Architectural Retiming: Pipelining Latency-Constrained Circuits}", booktitle = dac, month = jun, year = 1996 } @inproceedings{bommu97, author = {S. Bommu and M. Ciesielski and N. O'Neill and P. Kalla}, title = "{Sequential Logic Optimization with Implicit Retiming and Resynthesis}", booktitle = vlsi, year = 1997 } @inproceedings{singhal96, author = {V. Singhal and S. Malik and R. K. Brayton}, title = "{The Case for Retiming with Explicit Reset Circuitry}", booktitle = iccad, address = {San Jose, CA}, month = nov, year = 1996 } @article{romeo91, author = {Fabio Romeo and Alberto Sangiovanni-Vincentelli}, title = "A Theoretical Framework for Simulated Annealing", journal = "Algorithmica", year = 1991, } %%%%%%%%%%%%%%%%%%%%%%%%%5 @article{zhou-tcad-00, author = {H. Zhou and D. F. Wong and I. Liu and A. Aziz}, title = "{Simultaneous Routing and Buffer Insertion with Restrictions on Buffer Locations}", journal = ieeetcad, volume = 19, year = 2000, number = 7, month = jul, pages = {819-824} } @article{aziz-s1s-tcad-00, author = {A. Aziz and F. Balarin and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Sequential Synthesis Using {\tt S1S}}", journal = ieeetcad, volume = 19, year = 2000, number = 10, month = oct } @article{yuan-jetta-00, author = {J. Yuan and K. Schultz and C. Pixley and H. Miller and A. Aziz}, title = "{Automatic Vector Generation Using Constraints and Biasing}", journal = jetta, month = feb, year = 2000, pages = {107-120}, } @article{aziz-tocl-00, author = {A. Aziz and K. Sanwal and V. Singhal and R. Brayton}, title = "{Model-Checking Continuous Time Markov Chains}", journal = tocl, volume = 1, number = 1, month = jul, pages = {162-170}, year = 2000 } @article{aziz-cjtcs-00, author = {A. Aziz and F. Balarin and V. Singhal and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Equivalances for Fair Kripke Structures}", journal = cjtcs, year = 2003, note = {To appear}, } @article{aziz-fmsd-00, author = {A. Aziz and T. Shiple and V. Singhal and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Formula Dependent Equivalence for Compositional CTL Model Checking}", journal = fmsd, year = 2002, volume = 21, number = 2, pages = {193-224}, } @article{aziz-sat-tcad-00, author = {A. Aziz and J. Kukula and T. Shiple and J. Yuan}, title = "{Efficient Control State Space Search}", journal = ieeetcad, year = 2001, volume = 20, number =2, } @article{aziz-fac-00, author = {J. Kukula and T. Shiple and A. Aziz}, title = "{Techniques for Implicit State Enumeration of EFSMs}", journal = fac, year = 2004, note = {In press}, } @article{singhal-todaes-03, author = {V. Singhal and C. Pixley and A. Aziz and S. Qadeer and R. Brayton}, title = "{Sequential Optimization in the Absence of Global Reset}", journal = todaes, year = 2003, volume = 8, number = 2, month = apr, } @article{liu-todaes-00, author = {T. Liu and A. Aziz and V. Singhal}, title = "{Optimizing Designs Containing Black Boxes}", journal = todaes, year = 2002, volume = 6, number = 4, } @article{ganai-jetta-00, author = {M. Ganai and P. Yalagandula and A. Aziz and A. Kuehlmann and V. Singhal}, title = "{SIVA: A System for Coverage Directed State Space Search}", journal = jetta, year = 2001, month = feb, } @article{jason-fmsd-00, author = {J. Baumgartner and T. Heyman and V. Singhal and A. Aziz}, title = "{Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High Performance Netlists}", journal = fmsd, year = 2003, } @article{anuj-fmsd-03, author = {A. Goel and K. Sajid and H. Zhou and A. Aziz and V. Singhal}, title = "{BDD Based Procedures for a Theory of Equality with Uninterpreted Functions}", journal = fmsd, volume = {22}, pages = {204--224}, year = 2003, } @article{liu-tcad-00, author = {I. Liu and T. Chou and A. Aziz and D. F. Wong}, title = "{Zero-skew Clock Tree Construction by Simultaneous Routing, Wire Sizing, and Buffer Insertion}", journal = ieeetcad, year = 2000, note = {Under review}, } @article{zhou-buffer-tcad-00, author = {H. Zhou and A. Aziz}, title = "{Buffer Minimization