Abstract
The formal specification of hardware at the instruction level is a daunting task. The complexity, size and intricacies of most instruction sets makes this task even more difficult. However, the benefits of such a specification can be quite rewarding: a precise, unambiguous description is provided for each instruction, a basis for proving the correctness of code transformations is made available, and the specification can be animated, providing a simulator. This paper proposes a high level structural operational semantic (S.O.S.) specification for the class of transport triggered architectures. These architectures are simple, powerful, flexible and modular and can exploit very fine grained parallelism. The S.O.S. is novel in that it follows the structure of the architecture, and by doing so inherits the modularity of the architecture.
Chapter PDF
Similar content being viewed by others
References
Aiken, A. (1988), Compaction-Based Parallelization, PhD thesis, Department of Computer Science, Cornell University.
Boyer, R. S. and Yu, Y. (1996), `Automated proofs of object code for a widely used microprocessor’, Journal of the ACM 43(1), 166–192.
Corporaal, H. (1995), Transport Triggered Architectures: Design and Evaluation, PhD thesis, Technische Universiteit Delft.
Corporaal, H. and Mulder, H. J. M. (1991), Move: A framework for highperformance processor design, in `Supercomputing-91’, IEEE Computer Society Press, Albuquerque, New Mexico, pp. 692–701.
Corporaal, H. and van der Arend, P. (1993), `MOVE32INT, a sea of gates realization of a high performance transport triggered architecture’, MiModular operational semantic specification of transport triggered architectures 279 croprocessor and Microprogramming 38, 53–60.
Fisher, J. A., Ellis, J. R., Ruttenberg, J. C. and Nicolau, A. (1984), Parallel processing: A smart compiler and a dumb machine, in `Proceedings of the ACM SIGPLAN ‘84 Symposium on Compiler Construction’, Vol. 19 of SIGPLAN Notices, pp. 37–47.
Hannan, J. (1994), `Operational semantics-directed compilers and machine architectures’, Transactions on Programming Languages and Systems 16 (4), 1215–1247.
Hoogebrugge, J. (1996), Code Generation for Transport Triggered Architectures, PhD thesis, Technische Universiteit Delft.
Hunt, W. A. and Brock, B. C. (1989), The verification of a bit-slice ALU, in M. Leeser and G. Brown, eds, `Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects’, Vol. 408 of LNCS, Springer-Verlag, pp. 282–306.
Jones, G. and Sheeran, M. (1990), Circuit design in Ruby, in J. Staunstrup, ed., `Formal methods for VLSI design’, North-Holland, pp. 13–70.
Necula, G. C. and Lee, P. (1996), Safe kernel extensions without run-time checking, in `2nd Operating System Design and Implementation (OSDI)’, Seattle, Washington.
O’Donnell, J. T. (1992), Generating netlists from executable circuit specifications in a pure functional language, in J. Launchbury and P. Sansom, eds, `Functional Programming, Glasgow 1992’, Workshops in Computing, Springer-Verlag.
O’Leary, J., Linderman, M., Leeser, M. and Aagaard, M. (1993), HML: A hardware description language based on standard ML, in D. Agnew, L. Claesen and R. Camposano, eds, `Proceedings of the 11th IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL’93)’, IFIP, North-Holland, pp. 327–334.
Peterson, J., Hammond, K., Augustsson, L., Boutel, B., Burton, W., Fasel, J., Gordon, A. D., Hughes, J., Hudak, P., Johnsson, T., Jones, M., Peyton Jones, S., Reid, A. and Wadler, P. (1996), Report on the programming language Haskell (version 1.3), Technical Report YALEU/DCS/RR1106, Yale University.
Plotkin, G. D. (1981), A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark.
Plotkin, G. D. (1982), An operational semantics for CSP, Technical Report CSR-114–82, University of Edinburgh.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Mountjoy, J., Hartel, P., Corporaal, H. (1997). Modular Operational Semantic Specification of Transport Triggered Architectures. In: Kloos, C.D., Cerny, E. (eds) Hardware Description Languages and their Applications. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35064-6_22
Download citation
DOI: https://doi.org/10.1007/978-0-387-35064-6_22
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5387-5
Online ISBN: 978-0-387-35064-6
eBook Packages: Springer Book Archive