vlogsl swMATH ID: 12874 Software Authors: Katelman, Michael; Meseguer, José Description: vlogsl: a strategy language for simulation-based verification of hardware. 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 url{vlogsl}. url{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 url{vlogsl}, present several pedagogical examples using url{vlogsl}, and finally a larger example involving an open-source I\(^{2}\)C bus master. Homepage: http://link.springer.com/chapter/10.1007/978-3-642-19583-9_14 Related Software: Maude; Java+ITP; K Prover; Dist-Orc; MOMENT2; K tool; PVeStA; PMaude; MMT; Ptolemy; ITP/OCL; JavaFAN; Centaur; ACL2; Stratego; AProVE; ReSpecT; KOOL; Elf; SymPLFIED Cited in: 3 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year vlogsl: a strategy language for simulation-based verification of hardware. Zbl 1325.68150Katelman, Michael; Meseguer, José 2011 Cited by 3 Authors 3 Meseguer Guaita, José 1 Katelman, Michael 1 Roşu, Grigore Cited in 2 Serials 1 Information and Computation 1 The Journal of Logic and Algebraic Programming Cited in 2 Fields 3 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year