Occam in the specification and verification of microprocessors

1992 ◽  
Vol 339 (1652) ◽  
pp. 137-151 ◽  
Keyword(s):  
Programming Language ◽  
Vlsi Circuits ◽  
Hardware Verification ◽  
Floating Point ◽  
Algebraic Semantics ◽  
Levels Of Abstraction ◽  
Close Relationship ◽  
Floating Point Unit ◽  
Implementation Level ◽  
Formal Techniques

Occam is a parallel programming language which can be used to describe VLSI circuits at several levels of abstraction. For a given piece of hardware one might have one Occam description which is close to the implementation level and another which is close to a specification in a notation such as Z or CSP. Thus a design can be substantially verified by a proof of equivalence of such descriptions. This can sometimes be achieved by using transformations based on the algebraic semantics of Occam and, even where this is not possible, the clean design and semantics of Occam make other formal techniques either easier or more reliable. We discuss several case studies: the floating point unit of the IMS T800 transputer and various aspects of its successor, the IMS T9000. Despite the close relationship, on the surface, of these cases studies, radically different techniques were required for them. Based on this and other evidence, the author believes that one of the most important possessions when starting to tackle problems in hardware verification, at least at current levels of knowledge and technology, is an open mind.

scholarly journals Performance of an Occam/transputer implementation of interval arithmetic

1993 ◽  
Vol 22 (451) ◽  
Author(s):  
Ole Caprani ◽  
Kaj Madsen
Keyword(s):  
Programming Language ◽  
Interval Arithmetic ◽  
Assembly Language ◽  
Floating Point ◽  
Procedure Call ◽  
Floating Point Arithmetic ◽  
Floating Point Unit ◽  
On Chip ◽  
Point Arithmetic ◽  
Parameter Passing

<p>Rounded interval arithmetic is very easy to implement by means of directed rounding arithmetic operators. Such operators are available in the IEEE floating point arithmetic of the transputer. When a few small pieces of assembly language code are used to access the directed rounding operators, the four basic rounded interval arithmetic operators can easily be expressed in the programming language Occam.</p><p>The performance of this implementation is assessed and it is shown that the time consuming part of the calculation are not the directed rounding floating point operations as one might have expected. Most of the time is spent with transport of operands to and from the on-chip floating point unit and the procedure call/parameter passing overhead. Based on this experience the implementation is improved. This implementation runs with 0.15 MIOPS (Million Interval Operations Per Second) or 0.30 MFLOPS on an example interval calculation proposed by Moore. Furthermore, it is demonstrated that an advanced interval language compiler may provide a performance of 0.30 MIOPS or 0.59 MFLOPS on this example calculation.</p>

SIMD Multi Format Floating-Point Unit on the IBM z15(TM)

2020 ◽  
Author(s):  
Stefan Payer ◽  
Cedric Lichtenau ◽  
Michael Klein ◽  
Kerstin Schelm ◽  
Petra Leber ◽  
...  
Keyword(s):  
Floating Point ◽  
Floating Point Unit

scholarly journals Industrial hardware and software verification with ACL2

2017 ◽  
Vol 375 (2104) ◽  
pp. 20150399 ◽  
Author(s):  
Warren A. Hunt ◽  
Matt Kaufmann ◽  
J Strother Moore ◽  
Anna Slobodova
Keyword(s):  
Programming Language ◽  
Software Verification ◽  
Formal Analysis ◽  
Shared Vision ◽  
Theorem Prover ◽  
Software Systems ◽  
Levels Of Abstraction ◽  
Quarter Century ◽  
Industrial Use ◽  
Technical Features

The ACL2 theorem prover has seen sustained industrial use since the mid-1990s. Companies that have used ACL2 regularly include AMD, Centaur Technology, IBM, Intel, Kestrel Institute, Motorola/Freescale, Oracle and Rockwell Collins. This paper introduces ACL2 and focuses on how and why ACL2 is used in industry. ACL2 is well-suited to its industrial application to numerous software and hardware systems, because it is an integrated programming/proof environment supporting a subset of the ANSI standard Common Lisp programming language. As a programming language ACL2 permits the coding of efficient and robust programs; as a prover ACL2 can be fully automatic but provides many features permitting domain-specific human-supplied guidance at various levels of abstraction. ACL2 specifications and models often serve as efficient execution engines for the modelled artefacts while permitting formal analysis and proof of properties. Crucially, ACL2 also provides support for the development and verification of other formal analysis tools. However, ACL2 did not find its way into industrial use merely because of its technical features. The core ACL2 user/development community has a shared vision of making mechanized verification routine when appropriate and has been committed to this vision for the quarter century since the Computational Logic, Inc., Verified Stack. The community has focused on demonstrating the viability of the tool by taking on industrial projects (often at the expense of not being able to publish much). This article is part of the themed issue ‘Verified trustworthy software systems’.

Sign in / Sign up

Export Citation Format

Share Document