Degrees of formality in shallow embedding hardware description languages in HOL

Abstract

Theorem proving based techniques for formal hardware verification have been evolving constantly and researchers are getting able to reason about more complex issues than it was possible or practically feasible in the past. It is often the case that a model of a system is built in a formal logic and then reasoning about this model is carried out in the logic. Concern is growing on how to consistently interface a model built in a formal logic with an informal CAD environment. Researchers have been investigating how to define the formal semantics of hardware description languages so that one can formally reason about models informally dealt with in a CAD environment. At the University of Cambridge, the embedding of hardware description languages in a logic is classified in two categories: deep embedding and shallow embedding. In this paper we argue that there are degrees of formality in shallow embedding a language in a logic. The choice of the degree of formality is a trade-off between the security of the embedding and the amount and complexity of the proof effort in the logic. We also argue that the design of a language could consider this verifiability issue. There are choices in the design of a language that can make it easier to improve the degree of formality, without implying serious drawbacks for the CAD environment.

This research was sponsored by CNPq (Brazilian Government) and CHEOPS Project (ESPRIT BRA “3215”).