|
|
|---|
|
|
|
|---|
Automatic documentation support for svex symbolic test vectors.
Symbolic test vectors are integrated into ACL2::xdoc so that you can generate attractive explanations of your setup. This is often useful when communicating with logic designers.
NOTE: the topics here cover how we generate this documentation. If
you just want to document your own SVTVs, you don't need to know about any of
this—just give a
These functions don't do much error checking. We expect that we only are going to generate documentation after successfully processing the SVTV, so we generally just expect things to be well-formed at this point.
The XML we generate is not documented in ACL2::xdoc's xdoc::markup, and is not supported by tools like