The process terms are constructed compositionally following the structure of ELLA expressions. Primitive terms, corresponding to atomic operations in ELLA, are assembled using a small set of process compositions - process call, choice, causal product and hiding. The semantics of a Core ELLA expression is then taken to be the set of traces derived from the interpreted process term representing the expression.
This report is a semantics reference manual for ELLA, forming part of the reference material describing the ELLA language, together with the standard documents, i.e. language reference manual, tutorial and user guide. It is intended to complement rather than replace the standard ELLA documentation.` It has not been our intention to change the meaning of ELLA, but to capture its essence, representing the `understood' semantics exhibited by the standard commercial ELLA compiler and simulator. There are differences between this semantics and the `understood' semantics, but these arise due essentially to efficiency mechanisms introduced into the simulator. Although this report concentrates on ELLA, the techniques and semantic model used have wider application to other HDLs and digital systems, which will be the subject of future work.
This work has been conducted as part of a collaborative project sponsored by the DTI and SERC, involving Manchester, DRA (Malvern) and Harlequin Ltd. (Cambridge), with GEC Plessey Semiconductors (Swindon) as evaluators. Using the formal semantics as a basis, software tools for ELLA compilation, normalisation, (ground-term/symbolic) simulation, (enumerated/symbolic) verification and ELLA-to-ELLA rewriting have been implemented by the project partners, and embedded into an integrated ELLA Design and Verification Environment. The aim of the project has been to provide formal verification support tools which are amenable to the industrial hardware designer.