A temporal logic for data-flow VHDL

Author

Rodrigues, Vanderlei Moraes ; Wagner, Flavio Rech

Author_Institution

Inst. de Inf., Univ. Fed. do Rio Grande do Sul, Porto Alegre, Brazil

fYear

1998

fDate

30 Sep-3 Oct 1998

Firstpage

91

Lastpage

94

Abstract

This paper introduces a first-order linear-time temporal logic for two subsets of the VHDL. The subsets cover data-flow descriptions employing delta or inertial delays, and include signal attributes, generic parameters, and generate statements. The proofs in this logic are compositional, meaning we derive the properties of a design from the properties of its components. This paper also considers extensions to this logic, and compares it to related work. This logic is based on the UNITY formalism

Keywords

data flow computing; delays; formal verification; hardware description languages; temporal logic; UNITY formalism; compositional proofs; data-flow VHDL; data-flow descriptions; delta delays; first-order linear-time temporal logic; generic parameters; inertial delays; signal attributes; Computational modeling; Computer languages; Concurrent computing; Delay; Digital systems; Formal verification; Logic design; Logic programming; Read only memory; Signal generators;

fLanguage

English

Publisher

ieee

Conference_Titel

Integrated Circuit Design, 1998. Proceedings. XI Brazilian Symposium on

Conference_Location

Rio de Janeiro

Print_ISBN

0-8186-8704-5

Type

conf

DOI

10.1109/SBCCI.1998.715417

Filename

715417