%% 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 in Pass-transistor Logic}", journal = ieeetcad, month = may, year = 2001, } @inproceedings{liu-iccd-00, author = {I. Liu and A. Aziz}, title = "{Delay Constrained Optimization by Simultaneous Fanout Tree Construction, Buffer Insertion/Sizing and Gate Sizing}", booktitle = iccd, month = oct, year = 2000 } @article{rabin-jacm-89, author = {Michael O. Rabin}, title = {Efficient dispersal of information for security, load balancing, and fault tolerance}, journal = {Journal of the ACM}, volume = {36}, number = {2}, year = {1989}, pages = {335--348}, } @article{anderson-93-tacs, author = "T. Anderson and S. Owicki and J. Saxe and C. Thacker", title = "High-Speed Switch Scheduling for Local Area Networks", journal = "{ACM Transactions on Computer Systems}", month = nov, year = "1993", } @inproceedings{jason-cav-00, author = {J. Baumgartner and A. Tripp and A. Aziz and V. Singhal and F. Andersen}, title = "{An Abstraction Algorithm for the Verification of Generalized C-Slow Designs}", booktitle = cav, month = jul, year = 2000, pages = {5-19}, } @inproceedings{zhou-ispd-00, author = {H. Zhou and A. Aziz}, title = "{Buffer Minimization in Pass-transistor Logic}", booktitle = ispd, month = apr, year = 2000, pages = {105-110}, } @inproceedings{liu-ispd-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}", booktitle = ispd, month = apr, year = 2000, pages = {33-38}, } @inproceedings{yala-date-00, author = {P. Yalagandula and V. Singhal and A. Aziz}, title = "{Automatic Lighthouse Generation for Directed State Space Search}", booktitle = date, month = mar, year = 2000, pages = {237-242}, } @inproceedings{liu-date-00, author = {I. Liu and H. Zhou and M. Wong and A. Aziz}, title = "{Meeting Delay Constraints in DSM by Minimal Repeater Insertion}", month = mar, booktitle = date, year = 2000, pages = {436-440}, } @inproceedings{jason-cav-99, 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}", booktitle = cav, month = jul, year = 1999, pages= {72-83}, } @inproceedings{srinivasan-vlsidesign-99, author = {S. Srinivasan and P. Chhabra and P. Jaini and A. Aziz and L. K. John}, title = "{Formal Verification of a Snoop Based Cache Coherence Protocol using Symbolic Model Checking}", booktitle = vlsidesign, month = jan, year = 1999, pages = {288-293}, } @inproceedings{ganai-greatlakes-00, author = {M. Ganai and A. Aziz}, title = "{Rarity Based Guided State Space Search}", booktitle = greatlakes, month = mar, year = 2000, } @inproceedings{ganai-vlsidesign-02, author = {M. Ganai and A. Aziz}, title = "{Improved SAT-based Bounded Reachability Analysis}", booktitle = vlsidesign, month = jan, year = 2002, } @inproceedings{liu-vlsidesign-99, author = {T. Liu and M. Ganai and A. Aziz and J. Burns}, title = "{Performance Driven Synthesis for Pass-Transistor Logic}", booktitle = vlsidesign, month = jan, year = 1999, pages = {372-377}, } @inproceedings{shiple-srctechcon-93, author = {T. Shiple and A. Aziz and F. Balarin and S. Cheng and R. Hojati and T. Kam and S. Krishnan and V. Singhal and H. Wang and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Formal Design Verification of Digital Systems}", booktitle = "SRC TECHCON", month = sep, year = 1993 } @inproceedings{liu-iwls-99, author = {I. Liu and A. Aziz and M. Wong}, title = "{Buffering Large Networks by Lagrangian Relaxation}", booktitle = iwls, month = may, year = 1999 } @inproceedings{zhou-iwls-98, author = {H. Zhou and A. Aziz}, title = "{Buffer Minimization in Pass Transistor Logic}", booktitle = iwls, month = may, year = 1998, pages = {155-159}, } @inproceedings{liu-iwls-98, author = {I. Liu and T. Liu and H. Zhou and A. Aziz}, title = "{Simultaneous PTL Buffer Insertion and Sizing for Minimizing Elmore Delay}", booktitle = iwls, month = may, year = 1998, pages = {162-168}, } @inproceedings{tai-iwls-98, author = {T. Liu and A. Aziz and J. Burns}, title = "{Performance Driven Synthesis for Pass Transistor Logic}", booktitle = iwls, month = may, year = 1998, pages = {255-259}, } @inproceedings{chaudhry-iwls-98, author = {R. Chaudhry and T. Liu and A. Aziz and J. Burns}, title = "{Area Oriented Synthesis for Pass-Transistor Logic}", booktitle = iwls, month = may, year = 1998, pages = {169-176}, } @inproceedings{zhou-rr-iwls-98, author = {H. Zhou and V. Singhal and A. Aziz}, title = "{How Powerful is Retiming?}", booktitle = iwls, month = may, year = 1998, pages = {111-125}, } @inproceedings{ganai-iwls-98, author = {M. Ganai and A. Aziz}, title = "{Efficient Coverage Directed State Space Search}", booktitle = iwls, month = may, year = 1998, pages = {267-275}, } @inproceedings{hung-iwls-97, author = {W. Hung and A. Aziz and K. McMillan}, title = "{Heuristic Symmetry Reduction for Invariant Verification}", booktitle = iwls, month = may, year = 1997, } @inproceedings{aziz-tau-95, author = {A. Aziz and R. Brayton and F. Balarin and V. Singhal}, title = "{Timing-Safe Replaceability for Combinational Designs}", booktitle = tau, month = nov, pages = {121-128}, year = 1995 } @inproceedings{aziz-iwls-95, author = {A. Aziz and F. Balarin and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Synthesizing Interacting Finite State Machines}", booktitle = iwls, month = may, year = 1995 } @inproceedings{ranjan95, author = {R. Ranjan and A. Aziz and R. Brayton and B. Plessier and C. Pixley}, title = "{Efficient BDD Algorithms for FSM Synthesis and Verification}", booktitle = iwls, month = may, year = 1995, note = {Poster presentation}, } @inproceedings{aziz93a, author = {A. Aziz and S. Tasiran and R. Brayton}, title = "{BDD Variable Ordering for Systems of Interacting Finite State Machines}", booktitle = iwls, month = may, year = 1993, note = {Poster presentation}, } @techreport{singhal-tr-95, author = "V. Singhal and C. Pixley and A. Aziz and R.K. Brayton", title = "{Delaying Safeness for More Flexibility}", number = "UCB/ERL M95/5", institution = erl, address = {Univ. of California, Berkeley, CA 94720}, } @techreport{aziz94f, author = {A. Aziz and F. Balarin and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Synthesizing Interacting Finite State Machines}", number = {UCB/ERL M94/96}, institution = erl, address = {Univ. of California, Berkeley, CA 94720}, } @techreport{shiple-tr-94, author = "A. Aziz and T. Shiple and V. Singhal and R. Brayton and A. Sangiovanni-Vincentelli", title = "{Formula Dependent Equivalences for Compositional CTL Model Checking}", number = "UCB/ERL M95/78", institution = erl, address = {Univ. of California, Berkeley, CA 94720}, } @techreport{pixley-tr-94, author = {C. Pixley and V. Singhal and A. Aziz and R. Brayton}, title = "{Multi-Level Synthesis for Safe Replaceability}", number = {UCB/ERL M94/31}, institution = erl, } @techreport{tasiran-tr-93, author = {A. Aziz and S. Tasiran and R. Brayton}, title = "{BDD Variable Ordering for Interacting Finite State Machines}", number = {UCB/ERL M93/71}, institution = erl, address = {Univ. of California, Berkeley, CA 94720}, } @techreport{swamy-tr-93, author = {A. Aziz and V. Singhal and G. Swamy and R. Brayton}, title = "{Minimizing Interacting Finite State Machines}", number = {UCB/ERL M93/68}, institution = erl, address = {Univ. of California, Berkeley, CA 94720}, } @techreport{aziz-tr-93, author = {A. Aziz and V. Singhal and R. Brayton}, title = "{Verifying Interacting Finite State Machines: Complexity Issues}", number = {UCB/ERL M93/52}, institution = erl, address = {Univ. of California, Berkeley, CA 94720}, } @inproceedings{yuan-cav-97, author = {J. Yuan and J. Shen and J. Abraham and A. Aziz}, title = "{On Combining Formal and Informal Verification}", booktitle = cav, month = jul, year = 1997, pages = {376-387}, } @inproceedings{singhal-euro-dac-95, author = {V. Singhal and C. Pixley and A. Aziz and R. Brayton}, title = "{Exploiting Power-up Delay for Sequential Optimization}", booktitle = euro-dac, month = sep, year = 1995, pages = {54-59}, } @inproceedings{singhal-iccad-94, author = {C. Pixley and V. Singhal and A. Aziz and R. Brayton}, title = "{Multi-level Synthesis for Safe Replaceability}", month = nov, booktitle = iccad, year = 1994, pages = {442-449}, } @inproceedings{aziz-iccad95, author = {A. Aziz and F. Balarin and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Sequential Synthesis Using {\tt S1S}}", month = nov, booktitle = iccad, year = 1995, pages = {612-617}, } @inproceedings{aziz94c, author = {A. Aziz and V. Singhal and F. Balarin and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Equivalences for Fair Kripke Structures}", year = 1994, month = jul, booktitle = icalp, publisher = {Springer Verlag}, pages = {364-375}, } @techreport{aziz93b, author = {A. Aziz and V. Singhal and R. Brayton}, title = "{Verifying Interacting Finite State Machines}", number = {UCB/ERL M93/52}, institution = erl, address = {Univ. of California, Berkeley, CA 94720}, month = jul, year = 1993 } @inproceedings{aziz94e, author = { A. Aziz and V. Singhal and G. Swamy and R. Brayton}, title = "{Minimizing Interacting Finite State Machines: A Compositional Approach to Language Containment}", booktitle = iccd, pages = {255-261}, month = oct, year = 1994 } @inproceedings{aziz-dac-98, author = {A. Aziz and J. Kukula and T. Shiple}, title = "{Hybrid Verification Using Saturated Simulation}", booktitle = dac, month = jun, year = 1998, pages = {615-618}, } @inproceedings{liu-dac-97, author = {T. Liu and K. Sajid and A. Aziz and V. Singhal}, title = "{Optimizing Designs Containing Black Boxes}", booktitle = dac, month = jun, year = 1997, pages = {113-116}, } @inproceedings{luo-dac-98, author = {Y. Luo and T. Wongsonegoro and A. Aziz}, title = "{Hybrid Techniques for Fast Functional Simulation}", booktitle = dac, month = jun, year = 1998, pages = {664-667}, } @inproceedings{zhou-dac-99, author = {H. Zhou and M. Wong and I. Liu and A. Aziz}, title = "{Simultaneous Routing and Buffer Insertion with Restrictions on Buffer Locations}", booktitle = dac, month = jun, year = 1999, pages = {96-99}, } @inproceedings{chaudhry-iccd-98, author = {R. Chaudhry and T. Liu and A. Aziz and J. Burns}, title = "{Area Oriented Synthesis for Pass-Transistor Logic}", booktitle = iccd, month = oct, year = 1998, pages = {160-167}, } @inproceedings{kukula-fmcad-98, author = {J. Kukula and T. Shiple and A. Aziz}, title = "{Techniques for Implicit State Enumeration of EFSMs}", booktitle = fmcad, month = nov, year = 1998, pages = {469-482}, } @inproceedings{goel-cav-98, 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}", booktitle = cav, month = jul, year = 1998, pages = {244-255}, } @inproceedings{hsis-dac94, author = {A. Aziz and F. Balarin and R. Brayton and S. Cheng and R. Hojati and T. Kam and S. Krishnan and R. Ranjan and A. Sangiovanni-Vincentelli and T. Shiple and V. Singhal and S. Tasiran and H. Wang}, title = "{HSIS: A BDD-Based Environment for Formal Verification}", booktitle = dac, month = jun, year = 1994, pages = {454-459}, } @techreport{rajeev-tr-94, author = "R. Ranjan and A. Aziz and B. Plessier and C. Pixley and R. Brayton ", title = "{Efficient Formal Design Verification: Data Structure + Algorithms}", number = "UCB/ERL M94", institution = erl, address = {Univ. of California, Berkeley, CA 94720}, month = oct, year = 1994, } @inproceedings{malay-dac-99, author = {M. Ganai and A. Aziz and A. Kuehlmann}, title = "{Enhancing Simulation with BDDs and ATPG}", booktitle = dac, month = jun, year = 1999, pages = {385-390} } @inproceedings{aziz94d, author = {A. Aziz and S. Tasiran and R. Brayton}, title = "{BDD Variable Ordering for Interacting Finite State Machines}", booktitle = dac, month = jun, year = 1994, pages = {283-288}, } @inproceedings{aziz94b, author = {A. Aziz and T. Shiple and V. Singhal and A. Sangiovanni-Vincentelli}, title = "{Formula-Dependent Equivalence for Compositional CTL Model Checking}", booktitle = cav, month = jul, year = 1994, pages = {324-337}, } @inproceedings{aziz95a, author = {A. Aziz and F. Balarin and V. Singhal and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{The Temporal Logic of Stochastic Systems}", booktitle = cav, month = jul, year = 1995, pages = {155-165}, } @inproceedings{aziz95b, author = {A. Aziz and F. Balarin and M. DiBenedetto and R. K. Brayton and A. Saldanha and A. Sangiovanni-Vincentelli}, title = "{Supervisory Control of Finite State Machines}", booktitle = cav, month = jul, year = 1995, pages = {279-292}, } @inproceedings{aziz-cav-96, author = {A. Aziz and K. Sanwal and V. Singhal and R. Brayton}, title = "{Verifying Continuous Time Markov Chains}", booktitle = cav, month = jul, year = 1996, pages = {269-276}, } @inproceedings{short-vis-cav-96, author = {R. K. Brayton et al}, title = "{VIS: A system for Verification and Synthesis}", booktitle = cav, month = jul, year = 1996 } @inproceedings{vis-fmcad-96, author = { R. Brayton and G. Hachtel and A. Sangiovanni-Vincentelli and F. Somenzi and A. Aziz and S. Cheng and S. Edwards and S. Khatri and Y. Kukimoto and A. Pardo and S. Qadeer and R. Ranjan and S. Sarwary and T. Shiple and G. Swamy and T. Villa}, title = "{VIS}", booktitle = fmcad, month = nov, year = 1996 } @inproceedings{vis-cav-96, author = { R. Brayton and G. Hachtel and A. Sangiovanni-Vincentelli and F. Somenzi and A. Aziz and S. Cheng and S. Edwards and S. Khatri and Y. Kukimoto and A. Pardo and S. Qadeer and R. Ranjan and S. Sarwary and T. Shiple and G. Swamy and T. Villa}, title = "{VIS: A system for Verification and Synthesis}", booktitle = cav, month = jul, year = 1996, pages = {428-432}, } @techreport{aziz93d, author = {A. Aziz and S. Tasiran and R. K. Brayton}, title = "{BDD Variable Ordering for Interacting Finite State Machines}", number = {UCB/ERL M93/71}, institution = erl, address = {Univ. of California, Berkeley, CA 94720}, month = sep, year = 1993 } @techreport{aziz93c, author = {A. Aziz and V. Singhal and G. M. Swamy and R. K. Brayton}, title = "{Minimizing Interacting Finite State Machines}", number = {UCB/ERL M93/68}, institution = erl, address = {Univ. of California, Berkeley, CA 94720}, month = sep, year = 1993 } @phdthesis{aziz_thesis, author = {A. Aziz}, title = "{Formal Methods in VLSI System Design}", address = {Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720}, month = may, year = 1996 } @inproceedings{amit-iccad-97, author = {A. Mehrotra and S. Qadeer and V. Singhal and A. Aziz and R. Brayton and A. Sangiovanni-Vincentelli}, title = "{Sequential Optimisation without State Space Exploration}", booktitle = iccad, month = nov, year = 1997, pages = {208-215}, } @inproceedings{jun-iccad-99, author = {J. Yuan and K. Schultz and C. Pixley and H. Miller and A. Aziz}, title = "{Modeling Design Constraints and Biasing in Simulation Using BDDs}", booktitle = iccad, month = nov, year = 1999, pages = {584-589}, } @inproceedings{jun-iccad-03, author = {J. Yuan and K. Albin and A. Aziz and C. Pixley}, title = "{A Framework for Constrained Functional Verification}", booktitle = iccad, month = nov, year = 2003, } @inproceedings{jun-iccad-02, author = {J. Yuan and K. Albin and A. Aziz and C. Pixley}, title = "{Simplifying Boolean Constraint Solving in Random Simulation-Vector Generation}", booktitle = iccad, month = nov, year = 2002, } @inproceedings{liu-iccd-99, author = {I. Liu and A. Aziz and M. Wong and H. Zhou}, title = "{An Efficient Buffer Insertion Algorithm for Large Networks Based on Lagrangian Relaxation}", booktitle = iccd, month = oct, year = 1999, pages = {210-215}, } @misc{www-exam, author = {A. Aziz}, title = "{Exam Taking Tips}", howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/exam-tips.html+}" } @misc{www-writing, author = {A. Aziz}, title = "{How to Write Well}", howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/writing-tips.html+}" } @misc{www-presenting, author = {A. Aziz}, title = "{How to Present Well}", howpublished = "{\verb+http://www.ece.utexas.edu/~adnan/presentation-tips.html+}" } %%%%%%%%%%%%%%%%% NETWORKING @article{click-tocs-00, title = {The Click modular router}, author = {E. Kohler and R. Morris and B. Chen and J. Jannotti and M. F. Kaashoek}, journal = {ACM Transactions on Computer Systems}, volume = {18}, number = {3}, year = {2000}, month = {August}, pages = {263-297}, } @inproceedings{prakash-infocom-04, author = {A. Prakash and A. Aziz and V. Ramachandran}, title = "{Randomized Parallel Schedulers for Switch-Memory-Switch Routers: Analysis and Numerical Studies}", booktitle = infocom, year = 2004, } @inproceedings{prakash-infocom-02, author = {A. Prakash and S. Sharif and A. Aziz}, title = "{An $O(\lg^2 n)$ algorithm for output queuing}", booktitle = infocom, year = 2002, } @inproceedings{mckeown-infocom-96, author = {N. McKeown and V. Anantharam and J. Walrand}, title = "{Achieving 100\% throughput in an input-queued switch}", booktitle = infocom, year = 1996, } @article{mckeown-micro-97, title = {The Tiny Tera: a packet switch core}, author = {N. McKeown and M. Izzard and A. Mekkittikul and W. Ellersick and M. Horowitz}, journal = {IEEE Micro}, month = {January}, year = 1997, volume = {17}, number = {1}, pages = {27-33}, } @phdthesis{pankaj_thesis, author = {P. Gupta}, title = "{Algorithms for routing lookups and packet classification}", school = {stanford}, year = 2000 } @phdthesis{mckeown-thesis, author = {N. McKeown}, title = "{Scheduling algorithms for input switched queues}", school = ucb, year = 1995 } @inproceedings{gupta-networking-00, author = "P. Gupta and N. McKeown", title = "Dynamic Algorithms with Worst-Case Performance for Packet Classification", booktitle = "{IFIP Networking}", pages = "528-539", year = "2000", } @book{keshav97, author = {S. Keshav}, title = "{An Engineering Approach to Computer Networking}", publisher = "{Addison-Wesley}", year = 1997 } @inproceedings{lakshman-sigcomm-98, author = {T. Lakshman and D. Stiliadis}, title = "High-speed Policy-based Packet Forwarding Using Efficient Multidimensional Range Matching", booktitle = sigcomm, year = 1998 } @inproceedings{brodnik-sigcomm-97, author = {A. Brodnik and S. Carlsson and M. Degermark and S. Pink}, title = "Small Forwarding Tables for Fast Routing Lookups", booktitle = sigcomm, year = 1997 } @inproceedings{gupta-infocom-98, author = {P. Gupta and S. Lin and N. McKeown}, title = "{Routing Lookups in Hardware at Memory Access Speeds}", booktitle = infocom, year = "1998", } @inproceedings{balaji-infocom-00, author = {J. Dai and B. Prabhakar}, title = {The throughput of data switches with and without speedup}, booktitle = infocom, year = 2000, } @inproceedings{gupta-infocom-00, author = {P. Gupta and B. Prabhakar and S. Boyd}, title = "{Near Optimal Routing Lookups with Bounded Worst Case Performance}", booktitle = infocom, year = 2000 } @inproceedings{varghese-sigcomm-01, author = {F. Baboescu and G. Varghese}, title = "{Scalable Packet Classification}", booktitle = sigcomm, year = 2001 } @inproceedings{lampson-infocom-98, author = {B. Lampson and V. Srinivasan and G. Varghese}, title = "{IP Lookups using Multiway and Multicolumn Search}", booktitle = infocom, year = 1998 } @inproceedings{waldvogel-sigcomm-97, author = {M. Waldvogel and G. Varghese and J. Turner and B. Plattner}, title = "{Scalable High-Speed IP Routing Lookups}", booktitle = sigcomm, year = 1997 } @inproceedings{nilsson-98, author = {S. Nilsson and G. Karlsson}, title = "{Fast Address Lookup for Internet Routers}", booktitle = "{IFIP Intl.~Conf.~on Broadband Communications}", year = 1998 } @inproceedings{srinivasan-sigmetrics-98, author = {V. Srinivasan and G. Varghese}, title = "{Fast IP Lookups Using Controlled Prefix Expansion}", booktitle = sigmetrics, year = 1998 } @inproceedings{srinivasan-sigcomm-98, author = {V. Srinivasan and S. Suri and G. Varghese and M. Waldvogel}, title = "{Fast and scalable layer 4 switching}", booktitle = sigcomm, year = 1998 } @misc{www-intel-p4, author = {Intel}, howpublished = "{\tt developer.intel.com/design/Pentium4/prodbref/}" } @misc{www-laranetworks, author = {Inc., Lara Networks}, howpublished = "{\tt www.laranetworks.com}" } @misc{www-snort, howpublished = "{\tt www.snort.org}" } @misc{www-tarari, howpublished = "{\tt www.tarari.com}" } @misc{www-cudd, title = "{Colorado University Decision Diagram Package}", author = {Fabio Somenzi}, howpublished = "{\verb+http://vlsi.colorado.edu/~fabio/+}" } @misc{www-caida, author = {CAIDA}, howpublished = "{\tt www.caida.org}" } @article{shiloach-ipl-86, author = {A. Israeli and Y. Shiloach}, title = "{An Improved Parallel Algorithm for Maximal Matching}", journal = ipl, volume = "22", pages = "57-60", year = 1986, } @article{singhal-tcad-01, author = {V. Singhal and C. Pixley and A. Aziz and R. Brayton}, title = "{A Theory of Safe Replacements for Sequential Circuits}", journal = ieeetcad, volume = "20", number = 2, month = feb, year = 2001, } @article{bbn-ton-98, author = {C. Partridge and P. Carvey and E. Burgess and I. Castineyra and T. Clarke and L. Graham and M. Hathaway and P. Herman and A. King and S. Kohalmi and T. Ma and J. Mcallen and T. Mendez and W. Milliken and R. Pettyjohn and J. Rokosz and J. Seeger and M. Sollins and S. Storch and B. Tober and G. Troxel and D. Waitzman and S. Winterble}, title = "{A 50 Gbps IP router}", journal = ieeeton, volume = "6", number = "3", month = jun, year = 1998, } @article{keshav-ieeecomm-98, author = {S. Keshav and R. Sharma}, title = "{Issues and Trends in Router Design}", journal = ieeecomm, year = 1998, } @article{mckeown-ton-99, author = {N. McKeown}, title = "{iSLIP: A Scheduling Algorithm for Input-Queued Switches}", journal = ieeeton, volume = "7", number = "2", month = apr, year = 1999, } @article{karol-jsac-88, author = {M. Hluchyj and M. Karol}, title = "{Queueing in high-performance packet switches}", journal = jsac, volume = "6", number = "9", month = dec, year = 1988, } @article{prabhakar-jsac-97, author = {B. Prabhakar and R. Ahuja and N. McKeown}, title = "{Multicast Scheduling for Input-Queued Switches}", journal = jsac, volume = "15", number = "15", month = jun, year = 1997, } @article{chen-ton-00, author = {W.-T. Chen and C.-F. Huang and Y.-L. Chang and W.-Y. Hwang}, title = "{An Efficient Cell-Scheduling Algorithm for Multicast ATM Switching Systems}", journal = ieeeton, volume = "8", number = "4", month = aug, year = 2000, } @inproceedings{schultz-icc-94, author = {K. Schultz and P. Gulak}, title = "{Distributed Multicast Contention Using Content Addressable FIFOs}", booktitle = icc, year = 1994 } @article{hayes-comm-91, author = {J. Hayes and R. Breault and M. Mehmet-Ali}, title = "Performance Analysis of a Multicast Switch", journal = ieeetcom, volume = "39", number = "4", month = apr, year = 1991, } @article{chang-jcc-01-I, author = {C.-S. Chang and D.-S. Lee and Y.-S. Jou}, title = "{Load balanced Birkhoff-von Neumann switches, part I: one-stage buffering}", journal = "{Computer Communications}", year = 2001, } @article{chang-jcc-01-II, author = {C.-S. Chang and D.-S. Lee and C.-M. Lien}, title = "{Load balanced Birkhoff-von Neumann switches, part II: multi-stage buffering}", journal = "{Computer Communications}", year = 2001, } @inproceedings{kesidis-iscc-98, author = {A. Hung and G. Kesidis and N. McKeown}, title = "{ATM input buffered switches with the guaranteed rate property}", booktitle = ieeeiscc, year = 1998, } @inproceedings{chang-infocom-00, author = {C.-S. Chang and W.-J. Chen and H.-Y. Huang}, title = "{On service guarantees for input buffered crossbar switches: A capacity decomposition approach by Birkhoff and von Neumann}", booktitle = infocom, year = 2000, } @inproceedings{shah-infocom-02, author = {D. Shah and P. Giaccone and B. Prabhakar}, title = "Towards Simple, High-Performance Schedulers for High-aggregate bandwidth Switches", booktitle = infocom, year = 2002, } @inproceedings{marsan-infocom-01, author = {M. Marsan and A. Bianco and P. Giaccone and E. Leonardi and F. Neri}, title = "On the Throughput of Input-Queued Cell-Based Switches with Multicast Traffic", booktitle = infocom, year = 2001, } @inproceedings{chuang-infocom-99, author = {S.-T. Chuang and A. Goel and N. McKeown and B. Prabhakar}, title = "Matching Output Queueing with a Combined Input Output Queued Switch", booktitle = infocom, year = 1999, } @inproceedings{iyer-infocom-01, author = {S. Iyer and N. McKeown}, title = "Making parallel packet switches practical", booktitle = infocom, year = 2001, } @inproceedings{iyer-infocom-00, author = {S. Iyer and A. Awadallah and N. McKeown}, title = "Analysis of a Packet Switch with Memories Running at Slower than the Line Rate", booktitle = infocom, year = 2000, } @inproceedings{plotkin-soda-94, author = {T. Feder and N. Megiddo and S. Plotkin}, title = "A Sublinear Parallel Algorithm for Stable Matching", booktitle = soda, year = 1994, } @InBook{vazirani_survey, author = "V. Vazirani", chapter = "Parallel Graph Matching", note = "J. Reif (Editor)", title = "Synthesis of Parallel Algorithms", publisher = "Morgan-Kaufmann", year = "1993", pages = "783--812", } @book{diestel-graph-00, author = {R. Diestel}, title = "{Graph Theory}", publisher = "Springer Verlag", year = 2000, } @article{lev-tcomp-81, author = {G. Lev and N. Pippenger and L. Valiant}, title = "A Fast Parallel Algorithm for Routing in Permutation Networks", journal = tc, volume = "30", number = "2", month = feb, year = 1981, } @book{wegener-book, author = {I. Wegener}, title = "{Branching Programs and Binary Decision Diagrams}", publisher = "SIAM", year = 2000, } @book{perlman-book, author = {R. Perlman}, title = "{Interconnections}", publisher = "Addison Wesley", year = 2000, } @inproceedings{shashank-hoti-02, author = {S. Gupta and A. Aziz}, title = "{Multicast scheduling for switches with multiple input-queues}", booktitle = hoti, address = {Stanford University, CA}, month = aug, year = 2002 } @inproceedings{prakash-hoti-02, author = {A. Prakash and A. Aziz}, title = "{A middle ground between CAMs and DAGs for high-speed packet classification}", booktitle = hoti, address = {Stanford University, CA}, month = aug, year = 2002 } @inproceedings{prakash-hoti-01, author = {A. Prakash and A. Aziz}, title = "{OC-3072 Packet Classification Using BDDs and Pipelined SRAMs}", booktitle = hoti, address = {Stanford University, CA}, month = aug, year = 2001 } @InProceedings{peterson-dos-02, Author = "X. Qie and R. Pang and L. Peterson", Title = "{Defensive Programming: Using an Annotation Toolkit to Build Dos-Resistant Software}", booktitle = {Symposium on Operating Systems Design and Implementation}, address = {Boston, MA USA}, Month = "December", Year = 2002 } @book{peterson-book, author = {L. Peterson and B. Davie}, title = "{Computer Networks}", publisher = "Morgan-Kaufmann", year = 2000, } @article{turner-survey, author = {J. Turner and N. Yamanaka}, title = "{Architectural Choices in Large Scale ATM Switches}", journal = "{IEICE Transactions}", year = 1998, } @inproceedings{zhang-infocom-98, author = {D. Stephens and H. Zhang}, title = "{Implementing Distributed Packet Fair Queueing in a Scalable Switch Architecture}", booktitle = infocom, year = 1998 } @article{zhang-survey-95, author = {H. Zhang}, title = "{Service Disciplines For Guaranteed Performance Service in Packet-Switching Networks}", journal = pieee, volume = 83, number = 10, month = oct, year = 1995, } @misc{graham-69, author = {R. Graham}, journal = siam_am, title = "{Bounds on multiprocessor timing anomalies}", year = "1969" } @inproceedings{andrews-infocom-99, author = "M. Andrews and S. Khanna and K. Kumaran", title = "Integrated Scheduling of Unicast and Multicast Traffic in an Input-Queued Switch", booktitle = infocom, year = 1999 } @phdthesis{shashank-thesis, author = {S. Gupta}, title = "{Multicast scheduling for switches with multiple input-queues}", school = texas, year = 2001, } @article{bad-zhang-survey-95, author = {H. Zhang}, title = {Service Disciplines For Guaranteed Performance Service in Packet-Switching Networks}, journal = pieee, volume = 83, number = 10, month = oct, year = 1995, } @book{book-alon, author = {Noga Alon and Joel H. Spencer}, title = "{The Probabilistic Method}", publisher = "{Wiley, John \& Sons, Incorporated}", year = 2000 } @book{combinatorics-book, author = {J. van Lint and R. Wilson}, title = {A Course in Combinatorics}, year = 1992, publisher = {Cambridge University Press}, } @book{san-book2, author = {R. Barker and P. Massiglia and L. Krantz}, title = {Storage Area Networking Essentials}, year = 2001, publisher = {McGraw-Hill}, } @book{san-book, author = {M. Farley}, title = {Building storage area networks}, year = 2001, publisher = {McGraw-Hill}, } @book{optical-book, author = {T. Stern and K. Bala}, title = {Multiwavelength optical networks: a layered approach}, year = 1999, publisher = {Prentice-Hall}, } @inproceedings{ibm-hotchips-02, author = {F. Le Maut and G. Garcia}, title = {IBM PowerPRS: a scalable switch fabric}, booktitle = hotchips, address = {Stanford University, CA}, month = aug, year = 2002 } % Optical Networks: A Practical Perspective @book{optical-book-2, author = {R. Ramaswami and K. Sivarajan}, title = {Optical networks: a practical perspective}, year = 2001, publisher = {Morgan-Kaufmann}, } @book{tarjan-book, author = {R. Tarjan}, title = {Data structures and network algorithms}, publisher = siam, year = 1983, } @book{ids-book, author = {S. Northcutt and J. Novak}, title = {Network Intrusion Detection: An Analyst's Handbook}, publisher = {New Riders}, year = 2000, } @book{interconnection-networks, author = {J. Duato}, title = {Interconnection Networks}, publisher = {Morgan-Kaufmann}, year = 2002, } @book{infiniband, author = {W. Futral}, title = {InfiniBand Architecture: Development and Deployment--A Strategic Guide to Server I/O Solutions}, year = 2001, publisher = {Intel Press}, } @book{3gio, author = {A. Wilson and J. Schade and R. Thornburg}, title = {Introduction to PCI Express}, year = 2002, publisher = {Intel Press}, } @inproceedings{prakash-iwls-02, author = {A. Prakash and R. Kotla and T. Mandal and A. Aziz}, title = "A Reconfigurable Architecture and Associated Synthesis Methodology for High Speed Packet Classification", booktitle = iwls, year = 2002 } @article{prakash-tcad-03, author = {A. Prakash and R. Kotla and T. Mandal and A. Aziz}, title = "A High-performance Architecture and BDD-based Synthesis Methodology for Packet Classification", journal = ieeetcad, month = jun, year = 2003, volume = 83, number = 10, } @inproceedings{salil-focs-00, author = {O. Reingold and S. Vadhan and A. Wigderson}, title = "Entropy Waves, the Zig-Zag Graph Product, and New Constant-Degree Expanders and Extractors", booktitle = "{IEEE} Symposium on Foundations of Computer Science", pages = "3-13", year = "2000", } @article{yuan-dac-03, author = {J. Yuan and K. Albin and A. Aziz and C. Pixley}, title = "{Constraint Synthesis for Environment Modeling in Functional Verification}", journal=dac, year = 2003 } @inproceedings{kumar-ids-02, author = {P. Dokas and L. Ertoz and V. Kumar and A. Lazarevic and J. Srivastava and P.-N. Tan}, title = "{Data Mining for Network Intrusion Detection}", booktitle = "{Proc. NSF Workshop on Next Generation Data Mining}", year = 2002, } @inproceedings{inder-class-98, author = {I. Dhillon}, title = "{Visualizing Class Structure of Multidimensional Data}", booktitle = "{Symposium on the Interface}", month = may, year = 1998, } @inproceedings{paxson-02, author = {S. Staniford and V. Paxson and N. Weaver}, title = "{How to Own the Internet in Your Spare Time}", booktitle = "{USENIX Security Symposium}", year = 2002, } @article{cook-jsl-79, author = {S. Cook and R. Reckhow}, title = "{The Relative Efficiency of Propositional Proof Systems}", journal = jsl, volume = 44, number = 1, month = mar, year = 1979, pages = "36-50", } @article{haken-tcs-85, author = {A. Haken}, title = "{The Intractability of Resolution}", journal = tcs, volume = 39, month = mar, year = 1985, pages = "297-308", } @article{lingam-toplas-00, author = {G. Ramalingam}, title = "{Context-sensitive synchronization-sensitive analysis is undecidable}", journal = toplas, volume = 22, number = 2, year = 2000, pages = "416-430", } @inproceedings{ball-spin-00, author = "T. Ball and S. Rajamani", title = "Bebop: A Symbolic Model Checker for Boolean Programs", booktitle = "{SPIN}", pages = "113-130", year = "2000", } @inproceedings{reps-popl-95, author = "T. Reps and S. Horwitz and M. Sagiv", title = "Precise interprocedural dataflow analysis via graph reachability", booktitle = popl, year = 1995, } % generic abstraction paper @inproceedings{cousot-cav-02, author = {P. Cousot and R. Cousot}, title = {Software Analysis and Model Checking}, booktitle = cav, month = jul, pages = {37--56}, year = 2002, } @book{hilbert-10th, author = {Y. Matiyasevich}, title = {Hilbert's 10th Problem}, year = 1993, publisher = {MIT Press}, } @inproceedings{chase-vmcai-03, author = {N. Catano and M. Huisman}, title = {CHASE: A Static Checker for JML's Assignable Clause}, booktitle = vmcai, month = jan, pages = {26--40}, year = 2003, } @article{tip95survey, author = "F. Tip", title = "A survey of program slicing techniques", journal = "Journal of programming languages", volume = "3", pages = "121--189", year = "1995", } @inproceedings{wolper95, author = {P. Wolper and B. Boigelot}, title = "{An automata-theoretic approach to {Presburger} arithmetic constraints.}", booktitle = sas, pages = {21-32}, year = 1995 } @inproceedings{berkmin, author = "E. Goldberg and Y. Novikov", title = "BerkMin: A Fast and Robust SAT Solver", booktitle = date, year = "2002", } @inproceedings{shankar-lics-02, author = {N. Shankar}, title = "{Little Engines of Proof}", booktitle = lics, year = 2002 } @inproceedings{manku-cav-98, author = "G. Manku and R. Hojati and R. Brayton", title = "Structural Symmetry and Model Checking", booktitle = "Computer Aided Verification", pages = "159-171", year = "1998", } @inproceedings{prakash-spaa-03, author = {A. Aziz and A. Prakash and V. Ramachandran}, title = "{A near optimal scheduler for switch-memory-switch routers}", booktitle = spaa, month = jun, year = 2003 } %%%%%% ANALOG CAD references @inproceedings{coppejans-iccad-02, author = {P. Coppejans and W. De~Cock and P. Leroux and M. Steyaert}, title = "{Optimization of a Fully Integrated Low Power CMOS GPS Receiver}", booktitle = iccad, month = nov, year = 2002 } @inproceedings{koukab-iccad-02, author = {A. Koukab and K. Banerjee and M. Declercq}, title = "{Analysis and Optimization of Substrate Noise Coupling in Single-Chip RF Transceiver Design}", booktitle = iccad, month = nov, year = 2002 } @inproceedings{maria-iccad-02, author = {M. Hershenson}, title = "{Design of Pipeline Analog-to-Digital Converters Via Geometric Programming}", booktitle = iccad, month = nov, year = 2002 } @inproceedings{lemke-iccad-02, author = {A. Lemke and L. Hedrich and E. Barke}, title = "{Analog Circuit Sizing Based on Formal Methods Using Affine Arithmetic}", booktitle = iccad, month = nov, year = 2002 } @inproceedings{biagetti-iccad-02, author = {G. Biagetti and S. Orcioni and L. Signoracci and C. Turchetti and P. Crippa and M. Alessandrini}, title = "{SiSMA: A Statistical Simulator for Mismatch Analysis of MOS ICs}", booktitle = iccad, month = nov, year = 2002 } @inproceedings{balasa-iccad-02, author = {F. Balasa and S. Maruvada and K. Krishnamoorthy}, title = "{Efficient Solution Space Exploration Based on Segment Trees in Analog Placement with Symmetry Constraints}", booktitle = iccad, month = nov, year = 2002 } @inproceedings{razavi-dac-01, author = {J. Savoj and B. Razavi}, title = "{Design of Half-Rate Clock and Data Recovery Circuits for Optical Communication Systems}", booktitle = dac, month = jun, year = 2001 } @inproceedings{goren-dac-01, author = {D. Goren and E. Shamsaev and I. Wagner}, title = "{A Novel Method for Stochastic Nonlinearity Analysis of a CMOS Pipeline ADC}", booktitle = dac, month = jun, year = 2001 } @inproceedings{vemuri-dac-01, author = {S. Ganesan and R. Vemuri}, title = "{Behavioral Partitioning in the Synthesis of Mixed Analog-Digital Systems}", booktitle = dac, month = jun, year = 2001 } @inproceedings{gielen-dac-01, author = {W. Verhaegen and G. Gielen}, title = "{Efficient DDD-Based Symbolic Analysis of Large Analog Circuits}", booktitle = dac, month = jun, year = 2001 } @inproceedings{rutenbar-dac-00, author = {R. Phelps and M. Krasnicki and R. Rutenbar and L. Carley and J. Hellums}, title = "{A Case Study of Synthesis for Industrial-Scale Analog IP: Redesign of the Equalizer/Filter Frontend for an ADSL CODEC}", booktitle = dac, month = jun, year = 2000 } @inproceedings{vancoreland-dac-00, author = {P. Vancorenland and C. De Ranter and M. Steyaert and G. Gielen}, title = "{Optimal RF Design Using Smart Evolutionary Algorithms}", booktitle = dac, month = jun, year = 2000 } @inproceedings{ranter-dac-00, author = {C. De Ranter and B. De Muer and G. Van der Plas and P. Vancorenland and M. Steyaert and G. Gielen and W. Sansen}, title = "{CYCLONE: Automated Design and Layout of RF LC-Oscillators}", booktitle = dac, month = jun, year = 2000 } @inproceedings{coder-dac-00, author = {C. Guardiani and S. Saxena and P. McNamara and P. Schumaker and D. Coder}, title = "{An Asymptotically Constant, Linearly Bounded Methodology for the Statistical Simulation of Analog Circuits Including Component Mismatch Effects}", booktitle = dac, month = jun, year = 2000 } @inproceedings{shi-dac-00, author = {T. Pi and R. Shi}, title = "{Multi-Terminal Determinant Decision Diagrams: A New Approach to Semi-Symbolic Analysis of Analog Integrated Circuits}", booktitle = dac, month = jun, year = 2000 } @inproceedings{rutenbar-dac-99, author = {M. Krasnicki and R. Phelps and R. Rutenbar and L. Carley}, title = "{MAELSTROM: Efficient Simulation-Based Synthesis for Custom Analog Cells}", booktitle = dac, month = jun, year = 1999 } @inproceedings{vemuri-dac-99, author = {A. Doboli and A. Nunez-Aldana and N. Dhanwada and S. Ganesan and R. Vemuri}, title = "{Behavioral Synthesis of Analog Systems using Two-Layered Design Space Exploration}", booktitle = dac, month = jun, year = 1999 } @inproceedings{charbon-dac-98, author = {B. Arsintescu and E. Charbon and E. Malavasi and U. Choudhury and W. Kao}, title = "{General AC Constraint Transformation for Analog ICs}", booktitle = dac, month = jun, year = 1998 } @inproceedings{dunlop-dac-98, author = {A. Dunlop and A. Demir and P. Feldmann and S. Kapur and D. Long and R. Melville and J. Roychowdhury}, title = "{Tools and Methodology for RF IC Design}", booktitle = dac, month = jun, year = 1998 } % SESSION DESCRIPTION: % Performance space exploration for analog circuits is an important technique for % design and synthesis. The papers present novel contributions in this area, % including performance trade-off analysis, use of support vector machines and % geometric convex modeling. The final paper applies performance space modeling % for architectural selection of data converters. % % 1. Performance Trade-off Analysis of Analog Circuits By Normal-Boundary Intersection % Author(s): Guido Stehr, Helmut Graeb, Kurt Antreich % % 2. Support Vector Machines for Analog Circuit Performance Representation % Author(s):Fernando De Bernardinis, Michael Jordan, Alberto L. Sangiovanni-Vincentelli % % 3. Efficient Description of the Design Space of Analog Circuits % Author(s):Mar Hershenson % % 4. Architectural Selection of A/D Converters % Author(s):Martin Vogels, Georges G. Gielen @inproceedings{stehr-dac-03, author = {G. Stehr and H. Graeb and K. Antreich}, title = "{Performance Trade-off Analysis of Analog Circuits By Normal-Boundary Intersection}", booktitle = dac, month = jun, year = 2003 } @inproceedings{sangiovanni-dac-03, author = {F. De Bernardinis and M. Jordan and A. Sangiovanni-Vincentelli}, title = "{Support Vector Machines for Analog Circuit Performance Representation}", booktitle = dac, month = jun, year = 2003 } @inproceedings{maria-dac-03, author = {M. Hershenson}, title = "{Efficient Description of the Design Space of Analog Circuits}", booktitle = dac, month = jun, year = 2003 } @inproceedings{vogels-dac-03, author = {M. Vogels and G. Gielen}, title = "{Architectural Selection of A/D Converters}", booktitle = dac, month = jun, year = 2003 } %%% DAC 2002 % This session presents new developments in algorithms and methodology for % synthesis and systematic design of analog and mixed-signal circuits. Two % papers present progress in automatic model generation for synthesis. The % third paper presents exploration methods for high-level design of delta-sigma % modulators, and the final paper presents an A/D converter design case study.` @inproceedings{daems-dac-02, author = {W. Daems and G. Gielen and W. Sansen}, title = "{An Efficient Optimization--Based Technique to Generate Posynomial Performance Models for Analog Integrated Circuits}", booktitle = dac, month = jun, year = 2002 } @inproceedings{rutenbar-dac-02, author = {H. Liu and A. Singhee and R. Rutenbar and L. Carley}, title = "{Remembrance of Circuits Past: Macromodeling by Data Mining in Large Analog Design Spaces}", booktitle = dac, month = jun, year = 2002 } @inproceedings{gielen-dac-02, author = {O. Bajdechi and G. Gielen and J. Huijsing}, title = "{Optimal Design of Delta-Sigma ADCs by Design Space Exploration}", booktitle = dac, month = jun, year = 2002 } @inproceedings{adc-dac-02, author = {J. Vandenbussche and K. Uyttenhove and E. Lauwers and M. Steyaert and G. Gielen}, title = "{Systematic Design of a 200 Ms/s 8-bit Interpolating/Averaging A/D Converter}", booktitle = dac, month = jun, year = 2002 } @article{BHSA03, author = "Jason Baumgartner and Tamir Heyman and Vigyan Singhal and Adnan Aziz", month = "July", year = "2003", publisher = "Kluwer Academic Publisher", journal = "Formal Methods in System Design", volume = "23", number = "1", pages = "39--65", title = "An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists" } @phdthesis{gallager, author = "R. G. Gallager", title = "Low-density parity-check codes", school = "MIT, Cambridge, MA", year = "1962" } @inproceedings{bitfill, author = "Jorge Campeliot and Dharmendra S. Modha and Sridhar Rajagopalan", title = "Designing LDPC codes using bit-filling", booktitle = "IEEE International Conference on Communications", pages = {55-59}, month = "June", year = {2001} } @article{blanksby, author = "A. J. Blanksby and C. J. Howland", title = "A 690-mW 1-Gb/s 1024-b, rate-1/2 low-density parity-check decoder", journal = "IEEE Journal of Solid-State Circuits", volume = {37}, pages = {404-412}, month = "March", year = {2002} } @article{RiShUr01, author = "T. J. Richardson and M. A. Shokrollahi and R. L. Urbanke", title = "Design of capacity-approaching low density parity-check codes", journal = "IEEE Transactions on Information Theory", volume = {47}, month = "February", year = {2001} } @article{shanbhag, author = "M. Mansour and N. Shanbhag", title = "Architecture-aware low-density parity-check codes", journal = "IEEE International Symposium on Circuits and Systems", month = "May", year = {2003} } @article{shanbhag1, author = "M. Mansour and N. Shanbhag", title = "A novel design methodology for high performance programmable decoder cores for aa-ldpc codes", journal = "IEEE Workshop on Signal Processing Systems", month = "August", year = {2003} } @ARTICLE{braams:babel, AUTHOR = "Johannes Braams", TITLE = "Babel, a Multilingual Style-Option System for Use with LaTeX's Standard Document Styles", JOURNAL = {TUGboat}, VOLUME = {12}, NUMBER = {2}, PAGES = {291-301}, MONTH = "June", YEAR = {1991} } @INPROCEEDINGS{clark:pct, AUTHOR = "Malcolm Clark", TITLE = "Post Congress Tristesse", BOOKTITLE = "TeX90 Conference Proceedings", PAGES = "84-89", ORGANIZATION = "TeX Users Group", MONTH = "March", YEAR = {1991} } @ARTICLE{herlihy:methodology, AUTHOR = "Maurice Herlihy", TITLE = "A Methodology for Implementing Highly Concurrent Data Objects", JOURNAL = {ACM Trans. Program. Lang. Syst.}, VOLUME = {15}, NUMBER = {5}, PAGES = {745-770}, MONTH = "November", YEAR = {1993} } @book{bossert_book, author = "M. Bossert", title = "Channel Coding for Telecommunications", publisher = "John Wiley and Sons", month = "August", year = {1999} } @BOOK{Lamport:LaTeX, AUTHOR = "Leslie Lamport", TITLE = "LaTeX User's Guide and Document Reference Manual", PUBLISHER = "Addison-Wesley Publishing Company", ADDRESS = "Reading, Massachusetts", YEAR = "1986" } @BOOK{salas:calculus, AUTHOR = "S.L. Salas and Einar Hille", TITLE = "Calculus: One and Several Variable", PUBLISHER = "John Wiley and Sons", ADDRESS = "New York", YEAR = "1978" } @misc{ns-2, author = {ISI}, title = "The Network Simulator: NS-2", howpublished = "{\tt www.isi.edu/nsnam/ns}", } @misc{www-irvine-itr, author = {U. Irvine}, title = "Responding to Crises and Unexpected Events", howpublished = "{\tt www.itr-rescue.org}", } @inproceedings{estrin99next, author = "D. Estrin and R. Govindan and J. Heidemann and S. Kumar", title = "Next Century Challenges: Scalable Coordination in Sensor Networks", booktitle = "Mobile Computing and Networking", pages = "263--270", year = "1999", } @phdthesis{jianhua_thesis, author = {J. Gan}, title = "{Design and modeling of a 16-bit 1.5MSPS successive approximation ADC with non-binary capacitor array}", school = {The University of Texas at Austin}, month = dec, year = 2003 } @Book{leung02, author = "B. Leung", year = "2002", publisher = "Prentice-Hall", title = "VLSI for Wireless Communications", } @Book{cover_book, author = "T. Cover and J. Thomas", year = "1991", publisher = "Wiley Interscience", title = "Elements of Information Theory", } @inproceedings{wang-islped-01, author = "A. Wang and S. Chao and C. Sodini and A. Chandrakasan", title = "Energy efficient modulation and MAC for asymmetric RF microsensor system", booktitle = ispled, pages = "106--111", year = "2001", } @inproceedings{mohiyud-dac-05, author = {M. Mohiyuddin and A. Prakash and A. Aziz}, title = "{Synthesizing Interconnect-Efficient Low Density Parity Check Codes}", booktitle = dac, month = jun, year = 2005, } @article{bala-ton-97, author = "H. Balakrishnan and V. Padmanabhan and S. Seshan and R. Katz", title = "A comparison of mechanisms for improving {TCP} performance over wireless links", journal = "IEEE/ACM Transactions on Networking", volume = "5", number = "6", pages = "756--769", year = "1997",} @Book{security_book, author = "W. Stallings", year = "2002", publisher = "Prentice Hall", title = "Cryptography and Network Security: Principles and Practice", } @Book{adc_book, author = "R. Van de Plassche", year = "2003", publisher = "Kluwer Academic Publishers", title = "CMOS Integrated Analog-To-Digital and Digital-To-Analog Converters", } @Book{dally_book, author = "W. Dally and J. Poulton", year = "1998", publisher = "Cambridge University Press", title = "Digital Systems Engineering", } @inproceedings{schofield-isscc-03, author = {W. Schofield and D. Mercer and L. Onge}, title = "{A 16b 400MS/s DAC with $\less$80dBc IMD to 300MHz and $\less$160dBm/Hz noise power spectral density}", booktitle = isscc, month = feb, year = 2003, } @inproceedings{cong-isscc-03, author = {J. Cong and R. L. Geiger}, title = "{A 1.5 V 14 b 100 MS/s self-calibrated DAC}", booktitle = isscc, month = feb, year = 2003, } % above [1] and [2] are what we have discussed on Friday. Basically, a sub-DAC is % used to compensate the error of the main DAC, which is characterized at % power up by a high-resolution ADC. author = {H. Shin and D. Hodges}, title = "{A 250-Mbit/s CMOS Crosspoint Switch}", journal = jssc, volume = 24, number = 2, year = 1989 } @article{vassiliou-jsscc-03, author = {I. Vassiliou and K. Vavelidis and T. Georgantas}, title = "{A single-chip digitally calibrated 5.15~5.825-GHz 0.18 micron CMOS transceiver for 802.11a wireless LAN}", journal = jssc, volume = 38, number = 12, year = 2003 } % [3] involves techniques measures the mismatch of I/Q channels, and remove % the analog mismatch by post digital processing. This is different from % what I have told you on Friday. One Philips' DECT transceiver chip set % uses analog trimming with DAC controlled by the DSP (pp. 159-160, B. % Razavi, RF Microelectronics). % [4] Many sigma-delta ADCs move the design complexity from analog to % digital domain, taking advantage of low cost high speed digital circuits. % % [5] Many multi-level sigma-delta ADCs and DACs utilize digital shuffling % to move mismatch error to out of band of interest, thus mitigate the % stringent requirement of analog components. % [6] A. N. Karanicolas, Hae-Seung Lee, and K. L. Barcrania, "A 15-b % 1-Msample/s digitally self-calibrated pipeline ADC," IEEE J. Solid-State % Circuits, vol. 28, no. 12, pp. 1207-1215, Dec. 1993 @article{karanicolas-jsscc-93, author = {A. Karanicolas and H. Lee and K. Barcrania}, title = "{A 15-b 1-Msample/s digitally self-calibrated pipeline ADC}", journal = jssc, volume = 28, number = 12, year = 1993 } % [6] uses radix 1.93 instead of 2 pipeline stages to relax the matching % requirements of the analog components, and then use digital post % processing to obtain the correct results. @Book{gielen_book, author = "R. Rutenbar and G. Gielen and B. Antao", year = "2002", publisher = "Wiley Interscience", title = "Computer-Aided Design of Analog Integrated Circuits and Systems", } @inproceedings{carloni-dac-02, author = {A. Pinto and L. Carloni and A. Sangiovanni-Vincentelli}, title = "{Constraint-driven Communication Synthesis}", booktitle = dac, month = jun, year = 2002, } @inproceedings{carloni-iccd-03, author = {A. Pinto and L. Carloni and A. Sangiovanni-Vincentelli}, title = "{Efficient Synthesis of Networks On Chip}", booktitle = iccd, month = oct, year = 2003, } @article{cong-procieee-01, author = {J. Cong}, title = "{An Interconnect Centric Design Flow for Nanometer Technologies}", journal = pieee, volume = 89, number = 4, month = apr, year = 2001 } @inproceedings{dally-dac-01, author = {W. Dally and B. Towles}, title = "{Route Packets Not Wires: On chip Interconnection Networks}", booktitle = dac, month = jun, year = 2001, } @article{opasyn, author = {H. Koh and C. Sequin and P. Gray}, title = "{OPASYN: A Compiler for CMOS Operational Amplifiers}", journal = ieeetcad, month = feb, volume = 9, pages = {113-125}, number = 2, year = 1990 } @article{delight_spice, author = {W. Nye and D. Riley and A. Sangiovanni-Vincentelli and A. Tits}, title = "{DELIGHT.SPICE: An Optimization System for the Design of Integrated Circuits}", journal = ieeetcad, month = apr, volume = 7, pages = {501-518}, number = 4, year = 1988 } @article{rutenbar-tcad-96, author = {A. Ochotta and R. Rutenbar and L. Carley}, title = "{Synthesis of High Performance Analog Circuits in ASTRX/OBLX}", journal = ieeetcad, month = mar, volume = 15, pages = {273-293}, number = 3, year = 1996 } @article{gielen-jssc-89, author = {G. Gielen and H. Walscharts and W. Sansen}, title = "{ISAAC: A Symbolic Simulator for Analog Integrated Circuits}", journal = jssc, month = dec, volume = 24, number = 12, year = 1989 } @Book{convex_book, author = "R. Rockafellar", year = "1970", publisher = "Princeton Univesity Press", title = "Convex Analysis", } @Book{boyd_book, author = {S. Boyd and L. Vandenberghe}, year = "2005", publisher = "Cambridge Univesity Press", title = "Convex Optimization", url = "http://www.stanford.edu/~boyd/cvxbook.html", } @inproceedings{wu-fir, author = {S.-P. Wu and S. Boyd and L. Vandenberghe}, title = "{FIR filter design via spectral factorization and convex optimization}", url = "http://www.stanford.edu/~boyd/reports/magdes.pdf", } @inproceedings{boyd-iccad-98, author = {M. Hersheson and S. Boyd and T. Lee}, title = "{GPCAD: A Tool for CMOS Op-Amp Synthesis}", booktitle = iccad, month = nov, year = 1998, } @article{karp-tdb-04, author = {R. Karp and S. Shenker and C. Papadimitriou}, title = "{A Simple Algorithm for Finding Frequent Elements in Bags and Streams}", journal = "{ACM Transactions on Database Systems}", month = mar, year = 2004, number = 1, volume = 28, } @inproceedings{manku-vldb-04, author = {G. Manku and R. Motwani}, title = "{Approximate Counts and Quantiles over Sliding Windows}", booktitle = vldb, month = jun, year = 2004, } % Wegener, J., Sthamer, H., Jones, B. F., and Eyres, D. E. % Testing real-time systems using genetic algorithms. Software Quality 6 (1997), 127-135. @article{wegener-sq-97, author = {J. Wegener and H. Sthamer and B. Jones and D. Eyres}, title = "{Testing Real-time Systems Using Genetic Algorithms}", journal = "{Software Quality}", year = 1997, number = 6, } @article{sorkin-04, author = {A. Flaxman and A. W. Harrow and G. Sorkin}, title = "{Strings with maximum numbers of distinct subsequences and substrings}", journal = "{Electronic Journal of Combinatorics}", year = 2004, number = 1, volume = 11, }