Abstract
This paper is an approach to automated verification of circuits represented as switch-level designs. Switch-level models (SLM) are a well-established framework for modelling low-level properties of circuits. We use many-valued prepositional logic to represent a suitable variant of SLM. Logical properties of circuits (gate-level) can be expressed in a standard way in the same logic. As a result we can express soundness of switch-level designs wrt to gate-level specifications as many-valued deduction problems. Recent advances in many-valued theorem proving indicate that it is possible to handle real life examples. We report first results obtained with an experimental theorem prover.
Research supported by IBM Germany and Deutsche Forschungsgemeinschaft.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. E. Bryant and C.-J. H. Seger. Formal verification of digital circuits using symbolic ternary system models. In E. M. Clarke and R. P. Kurshan, editors, Computer-Aided Verification: Proc. of the 2nd International Conference CAV'90, pages 33–43. Springer, 1991.
R. Y. Bryant. A switch-level model and simulator for MOS digital systems. IEEE Transactions on Computers, C-33:160–169, 1984.
W. Büttner, K. Estenfeld, R. Schmid, H.-A. Schneider, and E. Tidén. Symbolic constraint handling through unification in finite algebras. Applicable Algebra in Engineering, Communication and Computing, 1:97–118, 1990.
H. Eveking. Verifikation digitaler Systeme:, eine Einführung in den Entwurf korrekter digitaler Systeme. LMI. Teubner, Stuttgart, 1991.
R. Hähnle. Towards an efficient tableau proof procedure for multiple-valued logics. In Proc. Workshop on Computer Science Logic, Heidelberg, pages 248–260. Springer, LNCS 533, 1990.
R. Hähnle. Uniform notation of tableaux rules for multiple-valued logics. In Proc. International Symposium on Multiple-Valued Logic, Victoria, pages 238–245. IEEE Press, 1991.
R. Hähnle. A new translation from deduction into integer programming. In Proc. Conf. on Artificial Intelligence and Symbolic Mathematical Computations, Karlsruhe. Springer LNCS, 1992.
R. Hähnle. Automated Proof Search in Multiple-Valued Logics. Oxford University Press, forthcoming, 1993.
R. Hähnle, B. Beckert, S. Gerberding, and W. Kernig. The Many-Valued Tableau-Based Theorem Prover 3 T AP. IWBS Report 227, Wissenschaftliches Zentrum Heidelberg, IWBS, IBM Deutschland, July 1992.
J. P. Hayes. A unified switching theory with applications to VLSI design. Proceedings of the IEEE, 70(10):1140–1151, October 1982.
J. P. Hayes. Pseudo-Boolean logic circuits. IEEE Transactions on Computers, C-35(7):602–612, jul 1986.
R. Smullyan. First-Order Logic. Springer, New York, 1968.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hähnle, R., Kernig, W. (1993). Verification of Switch-level designs with many-valued logic. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1993. Lecture Notes in Computer Science, vol 698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56944-8_50
Download citation
DOI: https://doi.org/10.1007/3-540-56944-8_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56944-2
Online ISBN: 978-3-540-47830-0
eBook Packages: Springer Book Archive