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 |