Abstract
This talk reports on the results of a 1 year collaborative research programme between B-Core(UK) Ltd and AWE (Aldermaston Weapon Establishment, Hunting-Brae) to develop an approach and a set of tools for the formal mathematical design and implementation of hardware circuits. The abstract specification and all designs are done within the framework of the B formal development method [2,3,4,5] and its supporting tools [1], while the hardware implementations are produced by utilizing the capabilities of VHDL [6,7] and its supporting synthesis tools [8].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
B-Core(UK) Limited. B-Toolkit User Manual Version 3.4 (available from B-Core (UK) Ltd. on request) (1996)
Abrial, J.-R.: The B Book – Assigning Programs to Meanings. Cambridge University Press, (1997), This book contains the mathematical basis for the B-Method
Abrial, J.-R., Lee, M.K.O., Neilson, D.S., Scharbach, P.N., Sørensen, I.H.: The B-method (software development). In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398–405. Springer, Heidelberg (1991)
Lano, K.: The B Language and Method. Springer, Heidelberg (1996)
Wordswoth, J.B.: Software Engineering with B. Addison-Wesley, (1996), This is the definitive guide to software engineering with B
Ashenden, P.J.: The Designer’s Guide to VHDL (1996)
IEEE. Standard VHDL Reference Manual, IEEE Standard 1076-1993 (1993)
TransEDA Limited. TransGATE VHDL for Synthesis (1992)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8) (1975)
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall International Series in Computer Science (1994)
He, J., Hoare, C.A.R., Sanders, J.W.: Data Refinement Refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sørensen, I.H. (1998). Using B to Specify, Verify and Design Hardware Circuits. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive