Principles of Verifiable RTL Design


Bibliography

The following bibliography entries are citations from the 2nd edition of Principles of Verifiable RTL Design. Where available at the time of this writing, this bibliography includes links to the papers and books.

[Abramovici et al 1990] M. Abramovici, M. A. Breuer, A. D. Friedman, Digital Systems Testing and Testable Design, IEEE Press, New York.

[Abts 1999] D. Abts, "Integrating Code Coverage Analysis into a large Scale ASIC Design Verification Flow," Proc. Intn'l HDL Conference, pp. 141-145, April, 1999.

[Amdahl 1967] G. M. Amdahl, "Validity of the Single Processor Approach to Achieving Large Scale Computing Capabilities," Proc. Spring Joint Computer Conference, pp. 483-485, 1967.

[Arnold et al 1998] M. G. Arnold, N. J. Sample, J. D. Schuler, Guidelines for Safe Simulation and Synthesis of Implicit Style Verilog, Proc. Intn'l Verilog HDL Conference, pp. 59-66, March, 1998.

[Ashar and Malik 1995] P. Ashar and S. Malik, "Fast functional simulation using branching programs," Proc. Intn'l Conf. on Computer-Aided Design, pp. 408-412, 1995.

[Barbacci and Siewiorek 1973] M. B. Barbacci and D. P. Siewiorek, "Automated Exploration of the Design Space for Register Transfer (RT) Systems," Proc. First Annual Symposium on Computer Architecture, December, 1973.

[Barnes and Warren 1999] P. Barnes, M. Warren, "A Fast and Safe Verification Methodology Using VCS, "Synopsys User's Group (SNUG99), Retrieved August 23, 1999 from the World Wide Web: http://www.synopsys.com/news/pubs/snug/snug99_papers/Barnes_Final.pdf

[Beizer 1990] B. Beizer, Software Testing Techniques, Van Nostrand Rheinhold, New York, second edition, 1990.

[Bening 1969] L. Bening, "Simulation of High Speed Computer Logic," Proc. Design Automation Workshop, pp. 103-112, June, 1969.

[Bening et al. 1982] L. Bening, T. A. Lane, C. R. Alexander, J. E. Smith, "Developments in Logic Network Path Delay Analysis," Proc. Design Automation Conference, pp. 605-615, June, 1982.

[Bening et al. 1997] L. Bening, T. Brewer, H. D. Foster, J. S. Quigley, R. A. Sussman, P. F. Vogel, and A. W. Wells, "Physical Design of 0.35m Gate Arrays for Symmetric Multiprocessing Servers," Hewlett-Packard Journal, pp. 95-103, April, 1997.

[Bening 1999a] L. Bening, "An RTL Design Verification Linting Methodology," Proc. Intn'l HDL Conference, pp. 136-140, April, 1999.

[Bening 1999b] L. Bening, "A Two-State Methodology for RTL Logic Simulation," Proc. Design Automation Conference, pp. 672-677, June, 1999.

[Bening and Chaney 2000] L. Bening, K. Chaney, Generation of reproducible random states in RTL simulator, Hewlett-Packard patent US06061819 05/09/2000.

[Bening 2001] L. Bening, B. Hornung, R. Pflederer, "Hardware Description Language-Embedded Regular Expression Support for Module Iteration and Interconnection," Proc. Intn'l HDL Conference, pp. 213-218, March, 2001.

[Bergeron 2003] J. Bergeron, Writing Testbenches : Functional Verification of HDL Models 2nd ed,  Springer, 2003.

[Berman and Trevillyan 1989] C. L. Berman and L. H. Trevillyan, "Functional Comparison of Logic Designs for VLSI Circuits," Proc. Intn'l. Conf. on Computer-Aided Design, pp. 456-537, 1989.

[Berge' et al. 1995] J.-M. Berge', O. Levia, J. Rouillard, "High-level System Modeling Specification Languages," in Current Issues in Electronic Modeling, Volume 3, pp. 51-75, Kluwer Academic Publishers, 1995.

[Blank 1984] T. Blank, "A Survey of Hardware Accelerators Used in Computer-aided Design," IEEE Design and Test, pp. 21-39, Aug., 1984.

[Brand 1993] D. Brand, "Verification of Large Synthesized Designs," Proc. Intn'l. Conf. on Computer-Aided Design, pp. 534-537, 1993.

[Brayton et al. 1996] R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G Swamy, T. Villa, "VIS: A System for Verification and Synthesis," Proc. Computer Aided Verification, 1996

[Breuer 1972] M. A. Breuer, "A Note on Three-valued Logic Simulation," IEEE Trans. on Computers, vol. C-21, pp. 399-402, Apr., 1972.

[Bryant 1986] R. Bryant, "Graph-based Algorithms for Boolean Function Manipulation," IEEE Trans. on Computers, Vol. C-35, No. 8, pp.677-69, 1986.

[Buchnik and Ur 1997] E. Buchnik, S. Ur, "Compacting regression-suites on-the-fly," Proceedings of the 4th Asia Pacific Software Engineering Conference, 1997.

[Burch and Singhal 1998] J. R. Burch and V. Singhal, "Tight Integration of Combinational Verification Methods," Proc. Intn'l Conf. on Computer-Aided Design, 1998.

[Cerny and Mauras 1990] E. Cerny and C. Mauras, "Tautology Checking Using Cross-controllability and Cross-Observability Relations," Proc. Intn'l. Conf. on Computer Aided Design, pp. 34-37, 1990.

[Cerny et al. 1998] E. Cerny, B. Berkane, P. Girodias, K. Khordoc, Hierarchical Annotated Action Diagrams, Kluwer Academic Publishers, 1998.

[Chappell 1999] B. Chappell, "The Fine Art of IC Design," IEEE Computer, pp. 30-34, July, 1999.

[Chappell and Yau 1971] S. G. Chappell and S. S. Yau, "A Three-Value Design Verification System," Proc. Fall Joint Computer Conference, pp. 651-661, 1971.

[Cheng and Krishnakumar 1993] K-T. Cheng, A. Krishnakumar, "Automatic Functional test Generation Using the Extended Finite State Machine Model." Proc. Design Automation Conference, pp. 86-91, June, 1993.

[Chu 1965] Y. Chu, "An Algol-like Computer Design Language," Communications of the ACM, pp.607-615, Oct. 1965.

[Clarke et al. 2000] E. Clarke, O. Grumberg, D. Peled, Model Checking, The MIT Press, 2000.

[Clarke, Emerson and Sistla1981] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Characterizing Properties of Parallel Programs as Fixpoints." Seventh Intn'l Colloquium on Automata, Languages, and Programming, volume 85 of LNCS, 1981.

[Clarke and Wing 1996] E. Clarke, J. Wing, "Formal Methods: State of the Art and Future Directions," CMU Computer Science Technical Report CMU-CS-96-178, August 1996

[Clarke and Kurshan 1997] E. Clarke, R. Kurshan, "Computer-Aided Verification," IEEE Spectrum, pp.61-67, June 1997.

[Devadas et al. 1996] S. Devadas, A. Ghosh, K. Keutzer, " An Observability-Based Code Coverage Metric for Functional Simulation," Proc. Intn'l Conf. on Computer-Aided Design, pp. 418-425, 1996.

[Dewey 1992a] A. Dewey ed. "Three Decades of HDLs Part 1: CDL Through TI-HDL," IEEE Design and Test, pp. 69-81, June, 1992.

[Dewey 1992b] A. Dewey ed. "Three Decades of HDLs Part 2: Conlan Through Verilog," IEEE Design and Test, pp. 54-63, September, 1992.

[Dietmeyer and Duley 1975] D. Dietmeyere, J. Duley, "Register Transfer Languages and Their Translation," In M. Breuer, Digital System Design Automation: Languages, Simulation & Data Base, pp. 117-218, Computer Science Press, Inc. 1975.

[Dill and Tasiran 1999] D. Dill, S. Tasiran, "Simulation meets formal verification," Proc. Intn'l Conf. on Computer-Aided Design, pp.221, 1999. Retrieved November 21, 1999 from Stanford University database on the World Wide Web: http://verify.stanford.edu/

[Duley and Dietmeyer 1968] J. Duley, D. Dietmeyer, "A Digital System Design Language (DDL)," IEEE Trans. on Computers, Vol.C-17, No. 9, pp. 850-861, Sept. 1968.

[Eichelberger and Williams 1977] E. B. Eichelberger and T. W. Williams, "A logic Design Structure for LSI Testability," Proc. Design Automation Conference, pp. 462-468, June, 1977.

[Ellsberger 1997] J. Ellsberger, D. Hogrefe A. Sarma, SDL: Formal Object-oriented Language for Communicating Systems, Prentice Hall, 1997.

[Eiriksson 1996] A. Eiriksson, "Integrating Formal Verification Methods with A Conventional Project Design Flow," Proc. Design Automation Conference, pp. 666-671, 1996.

[Fallah et al. 1998] F. Fallah, S. Devadas, K. Keutzer, "OCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional Verification," Proc. Design Automation Conference, pp.152-157, 1998.

[Foster 1998] H. D. Foster, "Techniques for Higher Performance Boolean Equivalence Verification," Hewlett-Packard Journal, pp. 30-38, August, 1998.

[Foster 1999] H. Foster "Formal Verification of the Hewlett-Packard V-Class Servers," Proc. DesignCon99 On-Chip Design Conference, pp. 107-119, January, 1999.

[Foster and Coelho 2001] H. Foster, C. Coelho, "Assertions Targeting A Diverse Set of Verification Tools," Proc. Intn'l HDL Conference, pp. 115-122, March, 2001.

[Grinwald et al. 1998] R. Grinwald, E. Harel, M. Orgad, S. Ur, A. Ziv, " User Defined Coverage - A tool Supported Methodology for Design Verification," Proc. Design Automation Conference, pp. 158-163, 1998.

[Gupta et al. 1997] A. Gupta, S. Malik, P. Ashar, "Toward Formalizing a Validation Methodology Using Simulation Coverage," Proc. Design Automation Conference, pp. 740-745, 1997.

[Hefferan et al. 1985] P. H. Hefferan, R. J. Smith, V. Burdick, D. L. Nelson, "The STE-264 Accelerated Electronic CAD System," Proc. Design Automation Conference, pp. 352-358, June, 1985.

[Hill and Peterson 1973] F. Hill, G. Peterson, Digital Systems: Hardware Organization and Design, Wiley, New York, 1973.

[Hitchcock 1982] R. B. Hitchcock, "Timing Verification and the Timing Analysis program," Proc. Design Automation Conference, pp. 594-604, June, 1982.

[Hoare 1981] C. A. R. Hoare, "The Emperor's Old Clothes," Communications of the ACM, February, 1981, pp. 75-83.

[Hoare 1998] C. A. R. Hoare, "The Logic of Engineering Design," Retrieved August 4, 1999 from the World Wide Web: http://www.comlab.ox.ac.uk/oucl/users/tony.hoare/logic1.html, March, 1998.

[Horgan et al. 1994] J. Horgan, S. London, M. Lyu, "Achieving Software Quality with Testing Coverage Measures," Computer, 27(9), pp. 60-69, September 1994.

[Howe 1997] H. Howe, "Pre- and Postsynthesis Simulation Mismatches," Proc. 6th International Verilog HDL Conference, March, 1997.

[Huang and Cheng 1998] S.Y. Huang and K.T. Cheng, Formal Equivalence Checking and Design Debugging, Kluwer Academic Publishers, 1998.

[Hughes 1958] B. Hughes, One of Minnesota's Newest Firms - Control Data Corporation, Minnesota Technolog, pp. 33-36, April, 1958.

[IEEE 1076 1993] IEEE Standard 1076-1993 VHDL Language Reference Manual, IEEE, Inc., New York, NY, USA, June 6, 1994.

[IEEE 1364 1995] IEEE Standard 1364-1995 IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language, IEEE, Inc., New York, NY, USA, October 14, 1996.

[IEEE 1364 2000] IEEE Proposed Standard 1364-2000 (Draft 5) IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language, IEEE, Inc., New York, NY, USA, March, 2000.

[IEEE 1364.1 1999] IEEE P1364.1/D1.4, Draft Standard for Verilog Register Transfer Level Synthesis, IEEE, Inc., New York, NY, USA, April 26, 1999.

[Iverson 1972] K.E. Iverson, "A Common Language for Hardware, Software, and Applications," Proceedings of the 1972 FJCC, pp.121-129, 1972.

[Jephson et al 1969] J. S. Jephson, R. P. McQuarrie, R. E. Vogelsberg, "A Three-value Design Verification System," IBM Systems Journal, Vol. 8, No. 3, pp. 178-188, 1969.

[Kang and Szygenda 1992] S. Kang and S. Szygenda, "Modeling and Simulation of Design Errors," Proc. of the Int'l Conference on Computer Design: VLSI in Computers and Processors, pp. 443-446, October 1992.

[Kantrowitz and Noack 1996] M. Kantrowitz, L. Noack, "I'm Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DECchip 21164 Alpha microprocessor," Proc. Design Automation Conference, pp. 325-330, 1996.

[Keating and Bricaud 1999] M. Keating and P. Bricaud, Reuse Methodology Manual, Kluwer Academic Publishers, 1999.

[Kleeman and Cantoni 1987] L. Kleeman and A. Cantoni, Metastable Behavior in Digital Systems, IEEE Design and Test, pp. 4-19, Dec., 1987.

[Kleinrock 1991] Networks". Kleinrock, "ISDN - The Path to Broadband Networks." Proc. IEEE, Feb. 1991, pp. 112-117.

[Krohn 1981] H. E. Krohn, "Vector Coding Techniques for High Speed Simulation," Proc. Design Automation Conference, pp. 525-529, 1981.

[Kuehlmann and Krohm 1997] A. Kuehlmann and F. Krohm, "Equivalence Checking Using Cuts and Heaps," Proc. Design Automation Conference, pp. 263-268, 1997.

[Kunz 1993] W. Kunz, "HANNIBAL: An Efficient Tool for Logic Verification Based on Recursive Learning, "Proc. Intn'l Conf. on Computer-Aided Design, pp. 538-543, 1993.

[Kurshan 1994] R. P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, 1994.

[Kurshan 1997] R. P. Kurshan, "Formal Verification in a Commercial Setting," Proc. Design Automation Conference, pp. 258-262, 1997.

[Malka and Ziv 1998] Y. Malka and Avi Ziv, " Design Reliability - Estimation Through Statistical Analysis of Bug Discovery Data," Proc. Design Automation Conference, pp. 644-649, June, 1998.

[Mangelsdorf et al. 1997] S. Mangelsdorf, R. Gratias, R. Blumberg, R. Bhatia, "Functional Verification of the HP PA 8000 Processor," Hewlett-Packard Journal, August, 1997.

[Matsunaga 1996] Y. Matsunaga, "An Efficient Equivalence Checker for Combinatorial Circuits," Proc, Design Automation Conference, pp. 629-634, 1996.

[McGeer et al. 1995] P. C. McGeer, K. L. McMillan, A.Saldanha, A. L. Sangiovanni-Vincentelli. and P.Scaglia, P., "Fast Discrete Function Evaluation Using Decision Diagrams," Proc. Intn'l Conf. on Computer-Aided Design, pp. 402-407, November, 1995.

[McMillan 1993] K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.

[McWilliams 1980] T. M. McWilliams, "Verification of Timing Constraints on Large Digital Systems," Proc, Design Automation Conference, pp. 139-147, 1980.

[Mills and Cummings 1999] D Mills and C. Cummings. "RTL Coding Styles That Yield Simulation and Synthesis Mismatches." Synopsys Users Group, San Jose, 1999. Retrieved August 3, 1999 from Synopsys database on the World Wide Web:
http://www.synopsys.com/news/pubs/snug/snug99_papers/Mills_Final.pdf

[Mittra 1999] S. Mittra, Principles of VERILOG PLI, Kluwer Academic Publishers, 1999.

[Murata 1989] T. Murata, Petri Nets: Properties, Analysis and Applications, Proc. IEEE, vol. 77, no. 1, pp. 541-580, Apr. 1989.

[OVI LRM 1993] Open Verilog International, Verilog Hardware Description Language Reference Manual (LRM) Version 2.0, March, 1993.

[Parnas 1972] D. L. Parnas, "On the Criteria to be Used in Decomposing Systems Into Modules," Communications of the ACM, Vol. 5, No 12, pp. 1053-1058, December 1972.

[Pfleeger 1998] S. L. Pfleeger, Software Engineering: Theory and Practice, Prentice Hall, 1998

[Ross and Goodenough 1975] D.T. Ross, J.B. Goodenough, C.A Irvin, "Software Engineering: Process, Principles, and Goals," IEEE Computer, Vol. 8, No. 5, pp. 17-27, May 1975.

[Rowson and Sangiovanni-Vincentelli 1997], J. Rowson, A. Sangiovanni-Vincentelli "Interface-based Design," Proc. Design Automation Conference, pp. 178-183, 1997.

[Sangiovanni-Vincentelli et al. 1996], A. Sangiovanni-Vincentelli, P. McGeer, A. Saldanh, "Verification of ElectronicSystems," Proc. Design Automation Conference, pp. 106-111, 1996.

[Seshu and Freeman 1962] S. Seshu and D. M. Freeman, "The Diagnosis of Asynchronous Sequential Switching Systems," IEEE Trans. on Elec. Computers, Vol 11, pp. 459-465, August, 1962.

[Seshu 1965] S. Seshu, "On an Improved Diagnosis Program," IEEE Trans. on Elec. Computers, Vol 12, pp. 76-79, February, 1965.

[Sutherland 1999] S. Sutherland, The Verilog PLI Handbook : A User's Guide and Comprehensive Reference on the Verilog Programming Language Interface, Kluwer Academic Publishers, Norwell, MA 02061, 1999.

[Szygenda 1972] S. A. Szygenda, "TEGAS2 -- Anatomy of a General Purpose Test Generation and Simulation System for Digital Logic," Proc. Design Automation Conference, pp. 116-127, June, 1972.

[Taylor et al. 1998] S. Taylor, M. Quinn, D. Brown, N. Dohm, S. Hildebrandt, J. Huggins, J. and C. Ramey, "Functional Verification of a Multiple-issue Out-of-order, Superscalar Alpha Processor -- the DEC Alpha 21264 microprocessor," Proc. Design Automation Conference, pp. 638-643, June, 1998.

[Thomas and Moorby 1998] D. E. Thomas and P. R.Moorby, The Verilog Hardware Description Language, Kluwer Academic Publishers, Norwell, MA 02061, pp. 136, 4th Edition, 1998.

[Ulrich 1965] E. G. Ulrich, "Time Sequenced Logical Simulation Based on Circuit Delay and Selective Tracing of Active Network Paths," Proc. ACM National Conference, pp. 437-448, 1965.

[Wilcox and Rombeck 1976] P. Wilcox and H. Rombeck, "F/Logic - An Interactive Fault and Logic Simulator for Digital Circuits," Proc, Design Automation Conference, pp. 68-73, 1976.