Abstract
The Accellera Property Specification Language (PSL) is designed for the formal specification of hardware. The Reference Manual contains a formal semantics, which we previously encoded in a machine readable version of higher order logic. In this paper we describe how to ‘execute’ the formal semantics using proof scripts coded in the HOL theorem prover’s metalanguage ML. The goal is to see if it is feasible to implement useful tools that work directly from the official semantics by mechanised proof. Such tools will have a high assurance of conforming to the standard. We have implemented two experimental tools: an interpreter that evaluates whether a finite trace w, which may be generated by a simulator, satisfies a PSL formula f (i.e. \(w \vDash f\)), and a compiler that converts PSL formulas to checkers in an intermediate format suitable for translation to HDL for inclusion in simulation test-benches. Although our tools use logical deduction and are thus slower than hand-crafted implementations, they may be speedy enough for some applications. They can also provide a reference for more efficient implementations.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfsthal, Y.: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000), www.haifa.il.ibm.com/projects/verification/RB_Homepage/ps/checkers.ps
Accellera home page, http://www.accellera.org
Accellera Property Specification Lanuage Reference Manual, Version 1.0, http://www.eda.org/vfv/docs/psl_lrm-1.0.pdf
Amjad, H.: Programming a symbolic model checker in a fully expansive theorem prover. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 171–187. Springer, Heidelberg (2003)
Barras, B.: Programming and computing in HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 17–37. Springer, Heidelberg (2000)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press/McGraw-Hill, Cambridge, Massachusetts (1990)
Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The prosper toolkit. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 78–92. Springer, Heidelberg (2000)
The Accellera Formal Property Language Technical Committee home page, http://www.eda.org/vfv
Comment on Ex 2, p 34, PSL RM v1.0, http://www.eda.org/vfv/hm/1017.html
Reply to Comment on Ex 2, p 34, PSL RM v1.0, http://www.eda.org/vfv/hm/1019.html
Gordon, M.J.C.: Validating the PSL/Sugar semantics using automated reasoning. Formal Aspects of Computing. Special issue on Semantic Foundations of Engineering Design Languages (to appear)
Gordon, M.J.C.: Using HOL to study Sugar 2.0 semantics. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, volume CP-2002-211736 of NASA Conference Proceedings, pp. 87–100 (2002), http://shemesh.larc.nasa.gov/tphols2002/proceedings.html
Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 1–15. Springer, Heidelberg (1998)
Proposal Presented to the Accellera Formal Verification Technical Committee, http://www.haifa.il.ibm.com/projects/verification/sugar/Sugar_2.0_Accellera.ps
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gordon, M., Hurd, J., Slind, K. (2003). Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive