Title :
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
fDate :
30 Sep-3 Oct 1998
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;
Conference_Titel :
Integrated Circuit Design, 1998. Proceedings. XI Brazilian Symposium on
Conference_Location :
Rio de Janeiro
Print_ISBN :
0-8186-8704-5
DOI :
10.1109/SBCCI.1998.715417
