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.
Author and article information
Dept. of Information Technology, Technical University of Denmark