Verifiable VHDL Generation with VMaude
	Download the VMaude semantics from here.
	Download the VMaude to VHDL Translator here.

		Behavior within a model checker, such as Maude, can be checked to meet some specification. We created VMaude, a VHDL-structured Maude framework. This allows you to write Maude behavior in VMaude, perform model checking, and automatically generate the corresponding VHDL module encoding the behavior.

Back to homepage. bak2007 {at} gmail.com 2009