This dissertation perceives a similarity between two activities: that of coordinating the search for simulation traces toward reaching verification closure, and that of coordinating the search for a proof within a theorem prover. The programmatic coordination of simulation is difficult with existing tools for digital circuit verification because stimuli generation, simulation execution, and analysis of simulation results are all decoupled. A new programming language to address this problem, analogous to the mechanism for orchestrating proof search tactics within a theorem prover, is defined wherein device simulation is made a first-class notion. This meta-language for functional verification is first formalized in a parametric way over hardware description languages using rewriting logic, and subsequently a more richly featured software tool for Verilog designs, implemented as an embedded domain-specific language in Haskell, is described and used to demonstrate the novelty of the programming language and to conduct two case studies. Additionally, three hardware description languages are given formal semantics using rewriting logic and we demonstrate the use of executable rewriting logic tools to formally analyze devices implemented in those languages. ; Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-11-20T20:25:10Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Katelman_Michael.pdf: 825730 bytes, checksum: 1dd49c7df9454c4f06119a974e1667a7 (MD5) ; Made available in DSpace on 2012-02-06T20:06:49Z (GMT). No. of bitstreams: 2 Katelman_Michael.pdf: 825730 bytes, checksum: 1dd49c7df9454c4f06119a974e1667a7 (MD5) license.txt: 4066 bytes, checksum: 9e4e282334b18ba28806ed4e2ba05422 (MD5)