Vlogsl: A strategy language for simulation-based verification of hardware

Michael Katelman, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationHardware and Software
Subtitle of host publicationVerification and Testing - 6th International Haifa Verification Conference, HVC 2010, Revised Selected Papers
Pages129-145
Number of pages17
DOIs
StatePublished - Mar 30 2011
Event6th International Haifa Verification Conference on Hardware and Software: Verification and Testing, HVC 2010 - Haifa, Israel
Duration: Oct 4 2010Oct 7 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6504 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th International Haifa Verification Conference on Hardware and Software: Verification and Testing, HVC 2010
CountryIsrael
CityHaifa
Period10/4/1010/7/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Vlogsl: A strategy language for simulation-based verification of hardware'. Together they form a unique fingerprint.

Cite this