Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96) (DCC)
Designing Correct Circuits
2 - 4 September 1996
Equivalence transformations are widely used in practical designs of VLSI circuits using Ruby. This paper demon-strates how proofs of these equivalences easily may be performed within a formal framework by a theorem prover. The proof tool used is called RubyZF and contains a semantical embedding of Ruby within Zermelo-Fraenkel set theory using the Isabelle theorem prover. The use of the system is exemplified by a concrete example taken from the T-Ruby design system.