{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/29614"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/29614","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"A meta-language for functional verification","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Katelman, Michael"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Meseguer, José","Mithal, Arvind","Roşu, Grigore","Torrellas, Josep"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012-02-06T20:06:49Z","date_published":"2012-02-06T20:06:49Z","updated_at":"2026-07-22T22:25:27Z","subjects":["Programming Languages","Formal Methods","Hardware Verification"],"languages":["en"],"rights":["Copyright 2011 Michael Katelman"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/29614","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José","Mithal, Arvind","Roşu, Grigore","Torrellas, Josep"]},{"key":"dc:creator","label":"Author","values":["Katelman, Michael"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2012-02-06T20:06:49Z","2011-12"]},{"key":"dc:type","label":"Dc Type","values":["Dissertation / Thesis","text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Programming Languages","Formal Methods","Hardware Verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2011 Michael Katelman"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/29614"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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)"]},{"key":"dc:title","label":"Title","values":["A meta-language for functional verification"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José","Mithal, Arvind","Roşu, Grigore","Torrellas, Josep"],"dc:creator":["Katelman, Michael"],"dc:date":["2012-02-06T20:06:49Z","2011-12"],"dc:description":["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)"],"dc:identifier":["http://hdl.handle.net/2142/29614"],"dc:language":["en"],"dc:rights":["Copyright 2011 Michael Katelman"],"dc:subject":["Programming Languages","Formal Methods","Hardware Verification"],"dc:title":["A meta-language for functional verification"],"dc:type":["Dissertation / Thesis","text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:27Z"}