A meta-language for functional verification

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2012

Author dc:creator

• Katelman, Michael

Contributors dc:contributor

• Meseguer, José
• Mithal, Arvind
• Roşu, Grigore
• Torrellas, Josep

• Programming Languages
• Formal Methods
• Hardware Verification

Statement dc:rights

• Copyright 2011 Michael Katelman

Language dc:language

en

Handle dc:identifier

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

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/29614