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}