Abstract
The paper presents the new computational model of Herbrand engines which combines finite-state control with uninterpreted data and function registers, thus yielding a finite representation of infinite-state machines. Herbrand engines are used to provide a high-level model of out-of-order execution in the design of micro-processors. The problem of verifying that a highly parallel design for out-of-order execution correctly implements the Instruction Set Architecture is reduced to establishing the equivalence of two Herbrand engines. We show that, for a reasonably restricted class of such engines, the equivalence problem is decidable, and present two algorithms for solving this problem.
Ultimately, the appropriate statement of correctness is that the out-of-order execution produces the same final state (and all relevant intermediate actions, such as writes to memory) as a purely sequential machine running the same program.
This research was supported in part by a gift from Intel, a grant from the Minerva foundation, and an Infrastructure grant from the Israeli Ministry of Science and the Arts.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G. Barrett and A. McIsaac. Model-checking in a microprocessor design project. In O. Grumberg, editor, Proc. 9 th Intl. Conference on Computer Aided Verification (CAV'97), Lect. Notes in Comp. Sci. Springer-Verlag, 1997. to appear.
R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(12):1035–1044, 1986.
J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In Proc. 6th Intl. Conference on Computer Aided Verification (CAV'94), volume 818 of Lect. Notes in Comp. Sci., pages 68–80. Springer-Verlag, 1994.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–l70, 1992.
Y.A. Chen, E.M. Clarke, P.-H. Ho, Y. Hoskote, T. Kam, M. Khaira, J.OLeary, and X. Zhao. Verification of all circuits in a floating point unit using word-level modelchecking. In M. Srivas and A. Camilleri, editors, Proc. 1st Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD'96), volume 1166 of Lect. Notes in Comp. Sci., pages 1–18. Springer-Verlag, 1996.
M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.
J.L. Hennessy and D.A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers Inc., San Francisco, California, 2nd edition, 1996.
R. Hojati, A. Isles, D. Kirkpatrick, and R.K. Brayton. Verification using uninterpreted functions and finite instantiations. In Proc. 1st Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD'96), pages 218–232, 1996.
R.B. Jones, D.L. Dill, and J.R.Burch. Efficient validity checking for processor verification. In Intl. Conf. on Computer-Aided Design. IEEE, 1995.
K. Keutzer. The need for formal methods for integrated circuit design. In M. Srivas and A. Camilleri, editors, Proc. 1st Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD'96), volume 1166 of Lect. Notes in Comp. Sci., pages 1–18. Springer-Verlag, 1996.
D.C. Luckham, D.M.R. Park, and M.S. Paterson. On formalized computer programs. J. Comp. Sys. Sci., 4(3):220–249, 1970.
Z. Manna and A. Pnueli. Synchronous schemes and their decision problems. In Proc. 7th ACM Symp. Princ. of Prog. Lang., pages 62–67, 1980.
S. Owre, J.M. Rushby, N. Shankar, and M.K. Srivas. A tutorial on using PVS for hardware verification. In R. Kumar and T. Kropf, editors, Proceedings of the Second Conference on Theorem Provers in Circuit Design, pages 167–188. FZI Publication, Universität Karlsruhe, 1994. Preliminary Version.
A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, Proc. 8th Intl. Conference on Computer Aided Verification (CAV'96), Lect. Notes in Comp. Sci., pages 184–195. Springer-Verlag, 1996.
M. Srivas and S. Miller. Applying formal verification to the aamp5 microprocessor: A case study in the industrial use of formal methods. J. on Formal Methods in System Design, 8:153–188, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, W., Pnueli, A., Ruah, S. (1998). Herbrand automata for hardware verification. In: Sangiorgi, D., de Simone, R. (eds) CONCUR'98 Concurrency Theory. CONCUR 1998. Lecture Notes in Computer Science, vol 1466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055616
Download citation
DOI: https://doi.org/10.1007/BFb0055616
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64896-3
Online ISBN: 978-3-540-68455-8
eBook Packages: Springer Book Archive