Advertisement

Component Reuse in B Using ACL2

  • Yann Zimmermann
  • Diana Toma
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)

Abstract

We present a new methodology that permits to reuse an existing hardware component that has not been developed within the B framework while maintaining a correct design flow. It consists of writing a specification of the component in B and proving that the VHDL description of the component implements the specification using the ACL2 system. This paper focuses on the translation of the B specification into ACL2.

Keywords

Clock Cycle Parallel Composition Register Transfer Level Component Reuse Hardware Description Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abrial, J.-R.: The B-Book – Assigning programs to meanings. CUP, Cambridge (1996)Google Scholar
  2. 2.
    Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Abrial, J.-R., Cansell, D., Méry, D.: A mechanically proved and incremental development of ieee 1394 tree identify protocol. Formal Aspects of Computing 14(3), 215–227 (2003)CrossRefGoogle Scholar
  4. 4.
    Aljer, A., Devienne, P., Tison, S., Boulanger, J.-L., Mariano, G.: B-HDL: Circuit Design in B. In: ACSD 2003, International conference on Application of Concurrency to System Design, pp. 241–242 (2003)Google Scholar
  5. 5.
    Dunne, S.: A Theory of Generalised Substitutions. In: Bert, D., Bowen, J. P., Henson, M. C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 270–290. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    European Organisation for Civil Aviation Equipment, http://www.eurocae.org/
  7. 7.
    Fox, A.C.J.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Fuchs, M., Mendler, M.: A Functional Semantics for Delta-Delay VHDL Based on FOCUS. In: Kloos, C.D., Breuer, P.T. (eds.) Formal Semantics for VHDL, pp. 9–42. Kluwer Academic Publishers, Dordrecht (1995)Google Scholar
  9. 9.
    Hallerstede, S., Zimmermann, Y.: Circuit Design by refinement in EventB. In: Proc. of FDL 2004 (2004)Google Scholar
  10. 10.
    Hazelhurst, S., Seger, C.-J.H.: Symbolic Trajectory Evaluation. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol. 1287, pp. 3–78. Springer, Heidelberg (1997)Google Scholar
  11. 11.
    IEEE (ed.): Standard VHDL - Language Reference Manual. IEEE Computer Society Press, USA (1988)Google Scholar
  12. 12.
    International Electrotechnical Commission, http://www.iec.ch/61508/
  13. 13.
    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided reasoning: ACL2 An approach, vol. 1. Kluwer Academic Publishers, Dordrecht (2000)Google Scholar
  14. 14.
    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided reasoning: ACL2 Case Studies, vol. 2. Kluwer Academic Publishers, Dordrecht (2000)Google Scholar
  15. 15.
    PUSSEE project IST-2000-30103 (2004), http://www.keesda.com/pussee/
  16. 16.
    Radio Technical Commission for Aeronautics, http://www.rtca.org/
  17. 17.
    Mermet, J.: UML-B - Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Bosten (2004) ISBN 1-4020-2866-0Google Scholar
  18. 18.
    Russinoff, D.M.: A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon Processor. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 3–36. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    SAE International. SAE J1708 revised OCT93, serial data communication between microcomputer systems in heavy-duty vehicule applications (1993), www.sae.org
  20. 20.
    Srivas, M., Rueß, H., Cyrluk, D.: Hardware Verification Using PVS. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol. 1287, pp. 156–205. Springer, Heidelberg (1997)Google Scholar
  21. 21.
    Toma, D., Borrione, D.: SHA formalization. In: ACL2 Workshop, USA (2003)Google Scholar
  22. 22.
    Toma, D., Borrione, D., Al-Sammane, G.: Combining several paradigms for circuit validation and verification. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 229–249. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. 23.
    Zimmermann, Y., Hallerstede, S., Cansell, D.: Formal modelling of electronic circuits using event-B, case study: SAE J708 serial communication link. In: Mermet, J. (ed.) UML-B - Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Boston (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Yann Zimmermann
    • 1
    • 2
  • Diana Toma
    • 3
  1. 1.KeesDA SAGièresFrance
  2. 2.MOSEL teamLORIAVandoeuvre-lès-Nancy CedexFrance
  3. 3.TIMAGrenoble CedexFrance

Personalised recommendations