Abstract
Data insensitive controllers (DICs) are systems where the datapath consists of assignment gates moving the integer data around, and latches storing the data. Memory controllers and communication systems are examples of DICs. In [HB95], it is proved that for DICs the property “when binary variable b becomes true, integer variables x and y are equal” can be proved by down-scaling the integer variables x and y to single-bit binary variables. In this paper, we generalize this notion and consider the problem of verifying properties of DICs in a linear temporal logic whose atomic propositions are finite variables and integer equalities. We show that for this temporal logic, one can always use finite instantiations, although the number of required bits varies with the complexity of the property.
Chapter PDF
Similar content being viewed by others
References
R. E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation”, IEEE Trans. on Computers, C-35(8): 677–691, August 1986.
R. Hojati, R. K. Brayton, “Automatic Datapath Abstraction In Hardware Systems”,Conference on Computer-Aided Verification, June 1995.
R. Hojati, R. Mueller-Thuns, P. Loewenstein, R. K. Brayton, “Automatic Verification of Memory System Using Language Containment and Abstraction”, Conference on Hardware Description Languages and Their Applications, 1995.
A. Isles, personal communication, 1995.
PowerPC94] IBM Microelectronics and Motorola, “PowerPC Microprocessor Family: The Programming Environment”,1994.
V. G. Vizing, “On an Estimate of the Chromatic Class of a p—Graph”, (in Russian), Diskret. Analiz., Vol. 3, 25–30 (1964).
P. Wolper, “Expressing Interesting Properties of Programs”, 13th Annual ACM Symp. on Principles of Prog. Languages, 1986.
P. Wolper, “The Tableau Method for Temporal Logic: An Overview”, Logique at Anal. 28, pp. 119–136, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Hojati, R., Dill, D.L., Brayton, R.K. (1997). Verifying linear temporal properties of data insensitive controllers using finite instantiations. In: Kloos, C.D., Cerny, E. (eds) Hardware Description Languages and their Applications. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35064-6_5
Download citation
DOI: https://doi.org/10.1007/978-0-387-35064-6_5
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5387-5
Online ISBN: 978-0-387-35064-6
eBook Packages: Springer Book Archive