vlogsl: A Strategy Language for Simulation-Based Verification of Hardware

  • Michael Katelman
  • José Meseguer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6504)


Languages such as SystemVerilog and e play an important role in contemporary hardware verification methodology. Through direct, language-level support for notions like constrained randoms, functional coverage, assertions, and so forth, they help verification engineers adopt useful paradigms. This paper demonstrates the usefulness of a new strategy-based paradigm for hardware test generation which is not directly supported by any language we are aware of. A strategy is formed by coordinating multiple simulations toward achieving a high-level goal, such as the generation of a targeted stimulus driving the device through a specific behavior. Strategies are made possible at the language level through constructs exerting meta-level control over simulation, making simulation traces first-class data objects that can be stored, queried, and otherwise manipulated programmatically. These ideas are embodied in a language and tool, called vlogsl. vlogsl is a domain-specific embedded language in Haskell, providing a sophisticated set of strategy language features, including first-order symbolic simulation and integration with an SMT solver. We motivate strategies, describe vlogsl, present several pedagogical examples using vlogsl, and finally a larger example involving an open-source I2C bus master.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Committee, I.R.: International Technology Roadmap for Semiconductors (2009),
  2. 2.
    Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI 2005), pp. 213–223. ACM, New York (2005)CrossRefGoogle Scholar
  4. 4.
    Gordon, M.J.C., Milner, R., Morris, L., Newey, M.C., Wadsworth, C.P.: A Metalanguage for Interactive Proof in LCF. In: Fifth Annual ACM Symposium on Principles of Programming Languages (POPL 1978), pp. 119–130 (January 1978)Google Scholar
  5. 5.
    Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)zbMATHGoogle Scholar
  6. 6.
    Grundy, J., Melham, T.F., O’Leary, J.W.: A reflective functional language for hardware design and theorem proving. Journal of Functional Programmming 16(2), 157–196 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Ho, P.H., Shiple, T.R., Harer, K., Kukula, J.H., Damiano, R.F., Bertacco, V., Taylor, J., Long, J.: Smart Simulation Using Collaborative Formal and Simulation Engines. In: Sentovich, E. (ed.) Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design (ICCAD-2000), pp. 120–126. IEEE, Los Alamitos (2000)Google Scholar
  8. 8.
    IEEE Standard for Verilog Hardware Description Language. IEEE Std 1364-2005 (2005)Google Scholar
  9. 9.
    Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodová, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414–429. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Katelman, M., Meseguer, J.: Source code for vlogsl HVC (2010),
  11. 11.
    Katelman, M., Meseguer, J.: A Strategy Language for Testing Register Transfer Level Logic. Technical report, Department of Computer Science, Univeristy of Illinois at Urbana-Champaign (June 2009)Google Scholar
  12. 12.
    Katelman, M., Meseguer, J., Escobar, S.: Directed-Logical Testing for Functional Verification of Microprocessors. In: 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008), pp. 89–100 (June 2008)Google Scholar
  13. 13.
    Khasidashvili, Z., Gavrielov, G., Melham, T.: Assume-guarantee validation for ste properties within an sva environment. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), pp. 108–115. IEEE, Los Alamitos (2009)CrossRefGoogle Scholar
  14. 14.
    King, J.C.: A New Approach to Program Testing. In: IBM 1974. LNCS, vol. 23, pp. 278–290. Springer, Heidelberg (1975)Google Scholar
  15. 15.
    King, J.C.: Symbolic Execution and Program Testing. Communications of the ACM 19(7), 385–394 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Meredith, P., Katelman, M., Meseguer, J., Roşu, G.: A Formal Executable Semantics of Verilog. In: 8th ACM & IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2010 (2010)Google Scholar
  17. 17.
    O’Sullivan, B., Stewart, D., Goerzen, J.: Real World Haskell. O’Reilly Media (2008),
  18. 18.
    Ouchet, F., Borrione, D., Morin-Allory, K., Pierre, L.: High-level symbolic simulation for automatic model extraction. In: Proceedings of the 2009 IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2009), pp. 218–221. IEEE Computer Society, Los Alamitos (2009)CrossRefGoogle Scholar
  19. 19.
    Seger, C.J.H., Jones, R.B., O’Leary, J.W., Melham, T.F., Aagaard, M., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. IEEE Trans. on CAD of Integrated Circuits and Systems 24(9), 1381–1405 (2005)CrossRefGoogle Scholar
  20. 20.

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Michael Katelman
    • 1
  • José Meseguer
    • 1
  1. 1.Department of Computer ScienceUniversity of Illinois at Urbana-ChampaignUrbanaUSA

Personalised recommendations