A meta-language for functional verification

Katelman, Michael

Permalink

https://hdl.handle.net/2142/29614 Copy

Description

Title

A meta-language for functional verification

Author(s)

Katelman, Michael

Issue Date

2012-02-06T20:06:49Z

Director of Research (if dissertation) or Advisor (if thesis)

Meseguer, José

Committee Member(s)

• Mithal, Arvind
• Roşu, Grigore
• Torrellas, Josep

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Programming Languages
• Formal Methods
• Hardware 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.

Graduation Semester

2011-12

Permalink

http://hdl.handle.net/2142/29614

Copyright and License Information

Copyright 2011 Michael Katelman

Owning Collections