Accellera Property Specification Language (PSL/Sugar) in HOL

.............................................................................
Frequently used acronyms (from http://www.deepchip.com/items/0423-14.html):
            PSL:  Property Specification Language
            OVL:  Open Verification Library (Verilog modules)
            OVA:  Open Vera Language
            SVA:  System Verilog Assertions
            SVL:  System Verilog assertion Library (SVA version of OVL)
.............................................................................

1. PSL Version 1.1 semantics in HOL and main properties proved [ postscript | pdf ].

2. PSL Version 1.01 semantics in HOL and main properties proved [postscript].

3. Property Specification Language Reference Manual, Version 1.1 (June 9, 2004). Final corrected version.

4. Accellera Technical Reports

5. Property Specification Language Reference Manual, Version 1.01 (April 25, 2003)

6. Archives of the PSL/Sugar online discussion (Accellera Formal Verification Technical Committee).

7. Archives of the SystemVerilog assertions online discussion (Accellera SystemVerilog Assertion Committee), slides from SystemVerilog Committee (December 4, 2002) and [sv-ac] revised semantics draft (dated 14 April 2003), SystemVerilog home page. FVTC Alignment Subcommittee final report on alignment of PSL and SVA.

8. Archives of the OVL online discussion (Open Verification Library (OVL) Technical Commitee), various documents and specifications including a tar-format directory containing checkers with PSL/Sugar and Verilog specifications and the OVL LRM.

9. Sugar homepage at IBM and PSL/Sugar Consortium homepage.

10. Legacy material:
    • Sugar 2.0 submission to Accellera
    • LRM Review Status Report
    • Proposal for Sugar 2.0 Temporal Layer Formal Syntax and Semantics (so called "SEM_1" semantics)

11. Index of /vfv/docs (collection of online documents from Accellera).

12. Category B TPHOLs2002 work-in-progress paper entitled Using HOL to study Sugar 2.0 semantics, published in NASA Conference Proceedings CP-2002-211736.
    
    [ postscript | pdf ]

13. A longer earlier draft of TPHOLs2002 Category B paper that contains a detailed (but now superceded) Sugar 2.0 semantics in higher order logic and (in an appendix) the buggy first attempt.
    
    [ postscript | pdf ]

14. A revised and extended version of the TPHOLs2002 Category B paper entitled Validating Sugar 2.0 semantics using automated reasoning with added introductory material, including a review of higher order logic and semantic embedding. A revised and updated version will be published in Formal Aspects of Computing for inclusion in the forthcoming special issue on Semantic Foundations of Engineering Design Languages (see below). Note that the semantics in the submitted version of the paper is not the latest version of the PSL/Sugar semantics, but the semantics in the version to be published (see next bulleted item) is.
    
    [ postscript | pdf ]

15. Final version of the paper, now entitled Validating the PSL/Sugar semantics using automated reasoning, to be published in Formal Aspects of Computing for inclusion in the forthcoming special issue on Semantic Foundations of Engineering Design Languages. Note that the semantics in this version of the paper corresponds to PSL Version 1.01.
    
    [ postscript | pdf ]

16. Poster for TPHOLs2002 (intended to be enlarged to A1 size, i.e. about 60x90 cm)
    
    [ postscript | pdf ]

17. Five minute presentation to precede poster session
    
    [ postscript | pdf ]

18. Draft version of a paper that, after revision, will appear in CHARME 2003 entitled Executing the formal semantics of the Accellera Property Specification Language by mechanised theorem proving by Mike Gordon, Joe Hurd and Konrad Slind (CHARME talk).
    
    [ postscript | pdf ]

19. Talk given at the Workshop on Semantics and Verification of Hardware and Software Systems
    [postscript for presentation |pdf for presentation |postscript for printing |4 slides per sheet postscript for printing |pdf for printing ]

20. Sugar 2 directory at SourceForge.

21. Latest versions of script files at Cambridge for building Sugar theories in HOL
    (these are work-in-progress and may be broken).

22. Some research project ideas on Sugar and HOL (likely to evolve).

23. IP Reuse Hardening via Embedded Sugar Assertions, Erich Marschner, Bernard Deadman, Grant Martin, IP Based SoC Design, Oct 30-31, 2002.
    
    [paper | slides]

24. Online stories:
    • free trial of IBM's FoCs tool for translating Sugar properties into HDL checkers
    • Accellera pushes for `unified assertions'
    • PSL + VHDL

25. Nice presentation by Michael Kohlhase on using XML for representing mathematical content (hopefully PSL/Sugar will eventually be defined in a machine processable format, see Sections 2.2 and 5.1 of this paper for motivation).

26. Description of ForSpec and discussion of abort constructs in Sugar and ForSpec.