Advertisement

Rewriting with constraints in T-ruby

  • Robin Sharp
  • Ole Rasmussen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

Abstract

This paper describes a tool for use in user-directed synthesis of circuits specified using the relational VLSI description language Ruby. The synthesis method is based on syntactic rewriting of Ruby terms, combined with the introduction of constraints into the specification. The rewriting process is described in a meta-language based on the use of tactics and tacticals, which makes it possible to develop complex specialised strategies for the refinement of specifications.

Keywords

Free Variable Theorem Prover Elsevier Science Publisher Identity Relation Proof Obligation 
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.

References

  1. 1.
    A. Church. The Calculi of Lambda-conversion. Princeton University Press, Princeton, New Jersey, 1941.Google Scholar
  2. 2.
    N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Science, Volume B: Formal Models and Semantics, chapter 6, pages 243–320. Elsevier Science Publishers B.V., 1990.Google Scholar
  3. 3.
    M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.Google Scholar
  4. 4.
    G. Jones and M. Sheeran. Circuit design in Ruby. In Jørgen Staunstrup, editor, Formal Methods for VLSI Design, pages 13–70. Elsevier Science Publishers B.V., 1990.Google Scholar
  5. 5.
    G. Jones and M. Sheeran. Relations and refinement in circuit design. In C. C. Morgan and J. C. P. Woodcock, editors, Proceedings of the 3rd. BCS FACS Workshop on Refinement, Workshops in Computing, pages 133–152, London, January 1991. BCS, Springer-Verlag.Google Scholar
  6. 6.
    P. Martin-Löf. Constructive mathematics and computer programming. In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 167–184. Prentice-Hall, London, 1985. Also published in Proc. 6th. International Congress for Logic, Methodology and Philosophy of Science, 153–175 (North-Holland, 1982).Google Scholar
  7. 7.
    L. C. Paulson. Logic and Computation, volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987.Google Scholar
  8. 8.
    Ole Rasmussen. A Ruby rewrite system. Master's thesis, Dept. of Computer Science, Technical University of Denmark, February 1992.Google Scholar
  9. 9.
    L. Rossen. Formal Ruby. In Jørgen Staunstrup, editor, Formal Methods for VLSI Design, pages 179–190. Elsevier Science Publishers B.V., 1990.Google Scholar
  10. 10.
    L. Rossen. Proving (facts about) Ruby. In G. Birtwhistle, editor, IV Higher Order Workshop, Banff, Workshops in Computing, pages 265–283. Springer-Verlag, 1990.Google Scholar
  11. 11.
    L. Rossen. Ruby algebra. In G. Jones and M. Sheeran, editors, Designing Correct Circuits, Oxford 1990, Workshops in Computing, pages 297–312. Springer-Verlag, 1990.Google Scholar
  12. 12.
    R. Sharp. T-Ruby: A tool for handling Ruby expressions. Technical Report ID-TR: 1992-112, Dept. of Computer Science, Technical University of Denmark, September 1992.Google Scholar
  13. 13.
    R. Sharp. The Ruby framework. Technical Report ID-TR: 1993-xx, Dept. of Computer Science, Technical University of Denmark, 1993. To appear.Google Scholar
  14. 14.
    R. Sharp and O. Rasmussen. Transformational rewriting with Ruby. In L. Claesen, editor, CHDL'93. IFIP WG10.2, Elsevier Science Publishers, B.V., 1993. To appear.Google Scholar
  15. 15.
    J. Smith. The identification of propositions and types in Martin-Löf's type theory: A programming example. In M. Karpinski, editor, Foundations of Computation Theory, volume 158 of Lecture Notes in Computer Science, pages 445–456, Berlin, 1983. Springer-Verlag.Google Scholar
  16. 16.
    D. Weise. Constraints, abstraction and verification. In M. Leeser and G. Brown, editors, Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of Lecture Notes in Computer Science, pages 25–39. Springer-Verlag, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Robin Sharp
    • 1
  • Ole Rasmussen
    • 1
  1. 1.Dept. of Computer ScienceTechnical University of DenmarkDenmark

Personalised recommendations