1This directory contains a deep embedding of the Accellera standard 2Property Specification Language (PSL/Sugar) Version 1.1 in HOL. 3 4The contents of this directory are 5 6README ......................... This file 7SyntaxScript.sml ............... Abstract syntax of core PSL 8ModelScript.sml ................ Theory of models 9ModelLemmasScript.sml .......... Properties of models and automata 10UnclockedSemanticsScript.sml ... Unclocked semantics 11ClockedSemanticsScript.sml ..... Clocked Semantics 12ExtendedSyntaxScript.sml ....... Abstract syntax of full PSL 13SyntacticSugarScript.sml ....... Semantics of full PSL 14RewritesScript.sml ............. Rewrites semantics of PSL 15LemmasScript.sml ............. Some lemmas from Eisner, Fisman, Havlicek 16ProjectionScript.sml............ Validation of the projection view (incomplete) 17 18Also needed is 19 20FinitePSLPathScript.sml ........... Theory of finite paths (lists) 21PSLPathScript.sml ................. Finite and infinite paths 22 23which are in the directory PSL/path 24(should be ../../path relative to this one). 25 26To run Holmake including the path directory, use: 27 28 Holmake -I ../../path 29 30[MJCG Sun Jan 16 2005: 31 Fixed to work with type variables introduced by Hol_datatype being in 32 alphabetic order] 33