On the Formal Derivation of a FEAL Microprocessor

Rimvydas Ruksenas
Kaisa Sere
Yi Zhao

In 6th NWPT, pages 332-345

Abstract:

We present an outline of a method for formal derivation of asynchronous VLSI circuits. The proposed method focuses on transformational style of the design and it uses techniques familiar from the construction of parallel programs. Refinement calculus and action systems are used as a framework for the design process. As a case study we look at the derivation of an asynchronous encryption/decryption microprocessor.

Comments
Åbo Akademi University, Department of Computer Science, FIN-20520 Turku, Finland, emails: {rruksena,zyi}@aton.abo.fi, University of Kuopio, Department of Computer Science and Applied Mathematics, FIN-70211 Kuopio, Finland, email: Kaisa.Sere@uku.fi, fax: +358-71-162595.

Available as PostScript, DVI.

BRICS WWW home page