1 2This directory contains a deep embedding of the Accellera standard 3Property Specification Language (PSL/Sugar) in HOL. 4 5The contents of this directory are 6 7README ......................... This file 8SyntaxScript.sml ............... Syntax of Sugar in HOL 9KripkeScript.sml ............... Theory of Kripke structures 10FinitePSLPathScript.sml ........ Theory of finite paths (lists) 11PSLPathScript.sml .............. Finite and infinite paths 12UnclockedSemanticsScript.sml ... Unclocked semantics 13ClockedSemanticsScript.sml ..... Clocked Semantics 14RewritesScript.sml ............. Rewrites semantics of Sugar 15PropertiesScript.sml ........... Proofs of properties of semantics 16 17As a result of trying to prove some `sanity checking' properties, bugs 18were found in the HOL semantics. Although the current semantics has 19been modified to correct all known bugs, the semantics is still 20evolving and should be regarded as provisional. The current draft 21documentation is at 22 23 http://www.eda.org/vfv/docs/formal_semantics_standalone.pdf 24 25This semantics has evolved considerably from the original one 26submitted to Accellera and appearing in the LRM. The changes, which 27make Sugar closer to ForSpec, has resulted in a much simpler 28semantics, and many proofs are now much shorter than before. 29 30The last round of analysis using HOL revealed two problems. 31 321. The rewrite and direct semantics differed for "f abort b". 33 This was fixed by restricting the requirement that the 34 two semantics agree to hold only for paths which the 35 current clock is true in the initial state. 36 372. The clocked and unclocked semantics of suffix implications {r}(f) 38 were incompatible. This was fixed by changing the clocked semantics. 39 40The main results in PropertiesTheory are as follows. 41 42SUMMARY OF MAIN PROPERTIES PROVED SO FAR 43======================================== 44 45Glossary 46-------- 47 48!x. P x All x: P x 49P ==> Q P implies Q 50|- P P proved by HOL 51 52ELEM w n nth element of w 53B_TRUE Boolean expression T 54B_SEM s b s |= b (semantics of Boolean expressions) 55US_SEM w r w |= r (unclocked semantics of SEREs) 56S_SEM w c r w |=c r (clocked semantics of SEREs) 57UF_SEM w f w |= f (unclocked formula semantics with |w|>0 for boolean formulas) 58OLD_UF_SEM w f w |= f (original LRM unclocked semantics of formulas) 59F_SEM w c f w |=c f (clocked semantics of formulas) 60S_CLOCK_FREE r SERE r contains no clocked sub-expressions 61F_CLOCK_FREE r Formula f contains no clocked sub-formulas 62S_CLOCK_COMP c r Result of applying official (LRM) PSL rewrites to SERE r@c 63F_CLOCK_COMP c f Result of applying official (LRM) PSL rewrites to formula f@c 64F_INIT_CLOCK_COMP c f Result of applying Eisner `abort-modified' PSL rewrites to f@c 65 66Properties proved 67----------------- 68 69S_SEM_TRUE_LEMMA 70|- !r w. S_CLOCK_FREE r ==> (S_SEM w B_TRUE r = US_SEM w r) 71 72F_SEM_STRONG_FREE_TRUE_LEMMA 73|- !f p. F_CLOCK_FREE f ==> (F_SEM p B_TRUE f = UF_SEM p f) 74 75S_CLOCK_COMP_ELIM 76|- !r w c. S_SEM w c r = US_SEM w (S_CLOCK_COMP c r) 77 78F_CLOCK_COMP_CORRECT 79|- !f w c. 80 B_SEM (ELEM w 0) c ==> (F_SEM w c f = UF_SEM w (F_CLOCK_COMP c f)) 81 82F_INIT_CLOCK_COMP_CORRECT 83|- !f w c. F_SEM w c f = UF_SEM w (F_INIT_CLOCK_COMP c f) 84 85INIT_CLOCK_COMP_EQUIV 86|- !f w c. 87 B_SEM (ELEM w 0) c 88 ==> 89 (UF_SEM w (F_CLOCK_COMP c f) = UF_SEM w (F_INIT_CLOCK_COMP c f)) 90 91OLD_UF_SEM_UF_SEM 92|- !f w. LENGTH w > 0 /\ F_CLOCK_FREE f ==> (OLD_UF_SEM w f = UF_SEM w f) 93 94(*****************************************************************************) 95(* ACKNOWLEDGEMENT *) 96(* The work here would not have been possible without the help of Cindy *) 97(* Eisner and Dana Fisman of IBM. They provided help when I was stuck, *) 98(* and suggested solutions to problems such as 1 and 2 above. *) 99(*****************************************************************************) 100 101MJCG 102Mon Jan 27 16:18:00 GMT 2003 103Wed Mar 19 20:18:45 GMT 2003