Advances in Hardware Design and Verification / Edition 1

by Hon Li, David Probst

Overview

CHARM '97 is the ninth in a series of working conferences devoted to the development and use of formal techniques in digital hardware design and verification. This series is held in collaboration with IFIP WG 10.5. Previous meetings were held in Europe every other year.

Product Details

ISBN-13:	9780412813306
Publisher:	Springer US
Publication date:	10/31/1997
Series:	IFIP Advances in Information and Communication Technology
Edition description:	1997
Pages:	313
Product dimensions:	6.10(w) x 9.25(h) x 0.03(d)

Read an Excerpt

Chapter 6 : A Polymoda Semantics For VHDL

S. Shankar and J. Slagle
Department of Computer Science, University of Minnesota
Minneapolis, MN, USA
[e-mail]
Abstract

This paper presents a formal semantics for a subset of VHDL that includes the basic control constructs, delta and unit delay signal assignment, variable assignment, and all forms of wait statements. A polymodal logic with two temporal modalities is used as the underlying formalism, thus allowing for formalization of the flows of time as well as control without modeling the simulation kernel. Since temporal logics are also good languages for specification of program properties and automated reasoning, this approach is a promising one for specification and verification of hardware expressed in VHDL.

1 INTRODUCTION

VHSIC Hardware Description Language (VHDL) is a widely used hardware description language which has become a standard in many domains. A common traditional use of VHDL has been to construct VHDL descriptions modeling the hardware design and then simulate the VHDL program to show that it meets a set of informal specification criteria from which test vectors have been generated. However, this approach is often insufficient in critical applications where it is desirable to prove that the VHDL description meets a set of formally specified correctness criteria, and a formal semantics of VHDL is thus needed.

There are many tradeoffs to consider when generating a formal semantics for VHDL. A short list of tradeoffs includes the following:

• What mathematical formalism is used to capture the semantics, and what are the theoretical properties of the formalism?
• How intuitive is the formalism as a language for expressing VHDL semantics?
• How simple is it to express the specification criteria that the VHDL model is intended to meet?
• Does the semantics model the simulation cycle or the hardware corresponding to the VHDL description?
• Is the translation from VHDL into the formalism automatable?
• How big (and useful) a subset of VHDL is supported? In particular, is the VHDL timing model completely supported?

The underlying formalism is of utmost importance in determining feasibility of formal verification. Most approaches involve the use of higher order logics (Reetz et al. 1995, VanTassel 1992), interval temporal logic (Wilsey 1992), process algebras (Borger et al. 1995, Goosens 1995), flow graphs (Deharbe et al. 1995), Petri Nets (Boussebha et al. 1992, Damm et al. 1993, Encrenaz et al. 1995, Olcoz et al. 1993), special purpose functional languages (Belhadj et al. 1993, Breuer et al. 1995, Fuchs et al. 1995, Salem et al. 1990), or various other formalisms (Hua et al. 1993). It is of course desirable to select a formalism that is suitable for formal verification. Additionally, it is desirable to select a simple formalism that allows for an intuitive VHDL semantics, since it may be difficult to determine if the semantics axe correct otherwise.

An overlooked criteria is the simplicity of the formalism in expressing properties that are to be proven. Temporal logic, either directly or through teinporal assertions integrated with graphical languages, has shown to be a good specification language. In fact, several approaches based on other formalisms use a specification related to temporal logic.

A major tradeoff is whether the semantics models the entire simulation cycle or the hardware corresponding to the VHDL description. Clearly, it is simpler to model a large VHDL subset if the semantics includes a formalization of the simulator. However, there is extra complexity involved in modeling the simulation engine. A related tradeoff is the nature of the translation from VHDL. Most existing approaches are automatable. A manual translation may suffer from bugs that axe introduced during translation.

The final tradeoff listed above relates to the size of the VHDL subset being formalized. VHDL is a large language, and all current formalizations thus select a subset. In particular, there are three distinct notions of flow in the VHDL timing model. First, there is unit delay which is used for signal assignments with explicit timing clauses, and corresponds to the actual time taken by the hardware entities being modeled. Second, there may be any number of delta delays within each clock time unit. The delta delay is an artifact of the simulation engine and relates to the event queue. Finally, the VHDL description can be considered as a parallel program, and the flow of control through this program constitutes a third type of flow that needs to be captured in the semantics.

Due to the difficulty of extracting all three types of flow in one formalism, most existing approaches either model the whole simulation engine or select a VHDL subset that eliminates either the delta delay or the unit delay. The former approach results in an excessively complicated model. In some cases, the latter approach is justifiable e.g. when it is intended for use with a synthesizable subset of VHDL that does not support delta delays. However, many existing VHDL descriptions use both forms of delays. The fundamental problem is the inability of the underlying logical formalism to capture all three notions of flow in a simple manner.

An interesting recent trend in logics is the use of polymodal logics for modeling multi-agent systems. Polymodal logics combine multiple modalities to provide a logic capable of expressing properties that deal with all of these modalities without resorting to a more complicated first order or higher order logic. Several such logics and combination techniques have been proposed (see for example (Finger et al. 1992, Finger et al. 1996, Kracht et al. 1991, Blackburn et at )). Two particularly common applications are:

• Logics combining time and belief modalities to model multi-agent systems where beliefs change over time.
• Logics combining transaction-time and valid-time modalities for modeling the evolution of temporal databases.

We believe that polymodal logics are also appropriate for expressing semantics of HDLs, due to the problem of capturing multiple flow notions discussed above.

In this paper we present a polymodal logic with two modalities, one for the flow of control through the parallel program and one for unit delay. First we present the syntax and semantics of the logic in Section 2. Then, section 3 presents the semantics of a VHDL subset in the polymodal logic. Last, we discuss our conclusions and further plans in Section 4.

2 POLYMODAL LOGIC

We first provide an intuitive explanation of the logic and then define its formal syntax and semantics.

The language of traditional unimodal linear time propositional temporal logic (PTL) augments propositional logic with the temporal operators: o (next), 0 (henceforth or always), 0 (eventually), A (atnext), and U (until). The o, 0, and 0 operators are unary future-only operators, while 0 and U are dyadic future-only operators. Time is a sequence of non-negative integers, with propositions taking on values that may be different at each timepoint. Such logics have been used to capture the semantics of parallel programs, with the flow of control through the program corresponding to the flow of time in the logic (Kroger 1987, Manna et at 1992). However, the addition of a clock-time modality as in VHDL makes such an approach inappropriate.

In our polymodal logic, there axe two independent dimensions: time and state. For each of the five PTL temporal operators, there is one operator for time and one for state, and the two are distinguished by an overscore for the state operator (e.g. o for next time and -6 for next state). Propositions take on values that may be different for each < time, state > pair. . . .

Table of Contents

Invited Lecture:

1 ASIC/system hardware verification at Nortel: a view from the trenches

PART ONE Advanced Processor Verification

3 Verifying out-of-order executions

PART TWO Semantics of Hardware-Description Languages

6 A polymodal semantics for VHDL