Design Verification Extra Readings Home Page

The lectures also cover the following papers for each indicated topic in class.

Combinational Logic Verification - SAT
1. "Using SAT for combinational equivalence checking," (pdf)
  Goldberg, E.I.; Prasad, M.R.; Brayton, R.K. Proc. Design, Automation and Test in Europe Conf., 2001. Page(s): 114 -121
2. "Chaff: engineering an efficient SAT solver," (pdf)
  Moskewicz, M.W.; Madigan, C.F.; Ying Zhao; Lintao Zhang; Malik, S. Proc. Design Automation Conference, 2001. Proceedings , 2001 Page(s): 530 -535
3. "GRASP: a search algorithm for propositional satisfiability," (pdf)
  Marques-Silva, J.P.; Sakallah, K.A. IEEE Transactions on Computers, Volume: 48 Issue: 5 , May 1999 Page(s): 506 -521
4. "Using Problem Symmetry in Search Based Satisfiability Algorithms." E. Goldberg, M. R. Prasad, and R. K. Brayton. Proc. Design, Automation, and Test in Europe Conf., pages 134-142, 2002.
Combinational Logic Verification - Implications
1. "HANNIBAL: An efficient tool for logic verification based on recursive learning," (pdf)
  Kunz, W. Proc. Intl Conf. Computer-Aided Design, 1993. Page(s): 538 -543
Combinational Logic Verification - BDD
1. "Efficient implementation of a BDD package," (pdf)
  Brace, K.S.; Rudell, R.L.; Bryant, R.E. Proc. Design Automation Conference, 1990. Page(s): 40 -45
2. "Efficient variable ordering heuristics for shared ROBDD," (pdf)
  Chung, P.-Y.; Hajj, I.M.; Patel, J.H. Proc. Intl Symp. Circuits and Systems, 1993., Page(s): 1690 -1693 vol.3
3. "Symmetry Detection And Dynamic Variable," (pdf)
  Panda, S.; Somenzi, F.; Plessier, B.F. Proc. Intl Conf. Computer-Aided Design, 1994., Page(s): 628 -631
4. "Efficient scheduling techniques for ROBDD construction," (pdf)
  Murgai, R.; Jain, J.; Fujita, M. Proc. Intl Conf. VLSI Design, 1999. Page(s): 394 -401
5. "Boolean satisfiability and equivalence checking using general binary decision diagrams," (pdf)
  Ashar, P.; Ghosh, A.; Devadas, S. Proc. Intl Conf. Computer Design: VLSI in Computers and Processors, 1991, Page(s): 259 -264
6. "Partitioned ROBDDs - a compact, canonical and efficiently manipulable representation for Boolean functions," (pdf)
  A. Narayan, J. Jain, M. Fujita, A. Sangiovanni-Vincentelli, Proc. Intl Conf. Computer-Aided Design, 1996. Page(s): 547 -554
Combinational Logic Verification - Incremental
1. "Verification of large synthesized designs," (pdf)
  Brand, D., Proc. Intl Conf. Computer-Aided Design, 1993. Page(s): 534 -537
2. "Efficient combinational verification using BDDs and a hash table," (pdf)
  Mukherjee, R.; Jain, J.; Takayama, K.; Fujitya, M.; Abraham, J.A.; Fussell, D.S. Proc. Intel Symp. Circuits and Systems, 1997, Page(s): 1025 -1028 vol.2
3. "VERILAT: verification using logic augmentation and transformations," (pdf)
  Paul, D.; Chatterjee, M.; Pradhan, D.K., IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, Volume: 19 Issue: 9 , Sept. 2000 Page(s): 1041 -1051
4. "Probabilistic design verification," (pdf)
  Jain, J.; Bitner, J.; Fussell, D.S.; Abraham, J.A., Proc. Intl Conf. Computer-Aided Design, 1991. Page(s): 468 -471
5. "Using global structural relationships of signals to accelerate SAT-based combinational equivalence checking," (pdf)
  R. Arora and M. S. Hsiao, Journal of Universal Computer Science, vol. 10, no. 12, pp. 1597-1628, December 2004.
Sequential Logic Verification
1. "A theory and implementation of sequential hardware equivalence," (pdf)
  C. Pixley, IEEE Trans. CAD, vol. 11, no. 12, Dec 1992, pp. 1469-1478.
2. "Principles of sequential-equivalence verification," M. N. Mneimneh and K. A. Sakallah, IEEE Design & Test of Computers, Vol. 22(3), 2005.
3. "Theory of safe replacements for sequential circuits," (pdf)
  V. Singhal, C. Pixley, A. Aziz, R.K. Brayton, IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 20, no. 2, Feb 2001, pp. 249-265.
4. "Reachability analysis using partitioned-ROBDDs," (pdf)
  Narayan, A.; Isles, A.J.; Jain, J.; Brayton, R.K.; Sangiovanni-Vincentelli, A.L., Proc. Intl Conf. Computer-Aided Design, 1997. Page(s): 388 -393
5. "Sequential equivalence checking based on structural similarities," (pdf)
  van Eijk, C.A.J., IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, Volume: 19 Issue: 7 , July 2000, Page(s): 814 -819
6. "AQUILA: an equivalence checking system for large sequential designs," (pdf)
  S.-Y. Huang; K.-T. Cheng; K.-C. Chen; C.-Y. Huang; Brewer, F., IEEE Transactions on Computers, Volume: 49 Issue: 5 , May 2000 Page(s): 443 -464
7. "On the verification of sequential equivalence,"
  J.-H R. Jiang and R. K. Brayton, IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, Volumne 22, No. 6, June 2003, pp. 686-697.
8. "Functional dependency for verification reduction,"
  J. H. R. Jiang, R. K. Brayton, Proc. CAV ’04, pp. 268-280.
9. "Fault-diagnosis-based technique for establishing rtl and gate-level correspondences," (pdf)
  Ravi, S.; Ghosh, I.; Boppana, V.; Jha, N.K. IEE Trans. Computer-Aided Design of Integrated Circuits and Systems, Volume: 20 Issue: 12 , Dec 2001, Page(s): 1414 -1425
Model Checking
1. "Application of temporal logic to the assistance of hardware logic design," (pdf)
  Fujita, M., Proc. Intl Symp. Multiple-Valued Logic, 1988, Page(s): 254 -263
2. "Symbolic model checking using SAT procedures instead of BDDs," (pdf)
  Biere, A.; Cimatti, A.; Clarke, E.M.; Fujita, M.; Zhu, Y., Proc. Design Automation Conference, 1999, Page(s): 317 -320
3. "Efficient preimage computation using a novel success-driven ATPG," (pdf)
  S. Sheng and M. S. Hsiao, Proceedings of the IEEE Design Automation and Test in Europe Conference, March 2003, pp. 822-827.
Simulation-based verification
1. "Design verification via simulation and automatic test pattern generation," (pdf)
  Al-Asaad, H.; Hayes, J.P. Proc. Intl Conf. Computer-Aided Design, 1995, Page(s): 174 -180
2. "High-level design verification of microprocessors via error modeling", (pdf)
  D. Van Campenhout, H. Al-Asaad, J. P. Hayes, T. Mudge, and R. Brown, ACM Transactions on Design Automation of Electronic Systems , 3(4), October 1998.
3. "OCCOM-efficient computation of observability-based code coverage metrics for functional verification," (pdf)
  Fallah, F.; Devadas, S.; Keutzer, K., IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, Volume: 20 Issue: 8 , Aug. 2001 Page(s): 1003 -1015
4. "A new simulation-based property checking algorithm based on partitioned alternative search space traversal,"
  Q. Wu and M. S. Hsiao, Proceedings of the IEEE High Level Design Validation and Test Workshop, November 2005, pp. 121-126.
5. "Cycle-based symbolic simulation of gate-level synchronous circuits,"
  V. Bertacco, M. Damiani, S. Quer, Proceedings of the IEEE Design Automation Conference, 1999, pp. 391-396.
Diagnosis
1. "ErrorTracer: design error diagnosis based on fault simulation techniques," (pdf)
  Shi-Yu Huang; Kwang-Ting Cheng, IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, Volume: 18 Issue: 9 , Sept. 1999 Page(s): 1341 -1352
2. "Modeling the unknown! Towards model-independent fault and error diagnosis," (pdf)
  Boppana, V.; Fujita, M., Proc. Intl Test Conference, 1998, Page(s): 1094 -1101
3. "On efficient error diagnosis of digital circuits," (pdf)
  N. Sridhar and M. S. Hsiao, Proc. International Test Conference, October, 2001, pp. 678-687.
4. "Error diagnosis of sequential circuits using region-based model," (pdf)
  A. L. D'Souza and M. S. Hsiao, Proc. IEEE VLSI Design Conference, January, 2001, pp. 103-108.