Svex-alist-to-verilog
Export an SVEX-ALIST to a Verilog file
Dumps a Verilog file based on a given sv::svex-alist
Use:
(svex-alist-to-verilog svex-alist
&key (output-file-name '"test")
(output-vars 'nil)
(out-wrappers 'nil)
(input-vars 'nil)
(env 'nil)
(assume ''t)
(export-to-svexl 'nil)
(sanity-check 't)
(skip-svex-simplify 'nil)
(skip-dumping-to-verilog 'nil))
This program dumps a Verilog file from a given svex-alist by simplifying
the given expressions based on user configurations. These can include binding
some input variables to contants, masking certain portions of the output,
simplifying expressions based on user-defined rewrite rules, and so on.
Example use:
(svl::svex-alist-to-verilog (sv::svtv->outexprs (evfalu-run))
:output-file-name "test"
:output-vars (my-out)
:out-wrappers '((my-out . (sv::partsel 4 4 my-out)))
:input-vars (srca)
:env `((srcb . 0) (srcc . 0) (srcd . 0))
:assume (and (equal (svl::bits srca 24 1) 0))
:skip-svex-simplify nil
:export-to-svexl *test-svexl*)
The arguments:
-
:output-file-name will be used to determine the name of the resulting Verilog
file and module name.
-
:output-vars should be the list of output-variables that will be included in
the output file.
-
:out-wrappers is an optional argument and can be used to wrap output
expressions inside other expressions. This can be useful for when selecting a
certain portion of the output. In the example above, only my-out[7:4] will
appear in the output file.
-
:input-vars is a list of input variables that needs to be left as a free
variable. When nothing is provided, the program will use all available
variables.
-
:env can be used to bind variables to constants. If a variable is bound to a
constant, and :input-vars includes it in its list, then :input-vars will
override it unless :input-vars is nil.
-
:assume should be an untranslated term that the user wants to assume during
simplification. The assumptions given are not guaranteed to be applied. Adding
rewrite rules for svex-simplify might help in those cases.
-
:sanity-check is highly recommended. There are 2 components in this program
whose soundness are in question. First one is svex-simplify, which
uses ACL2::rp-rewriter to conduct its simplifications with some wrappers
around it. Even though rp::rp-rewriter is verified, that surrounding program
might be buggy. The second part that might have soundness bugs is the part of
the program that creates the resulting Verilog file content. The sanity check
mechanism makes sure that the resulting file is functionally equivalent to the
input expressions under the given user configurations. Sanity check is
performed by parsing the output file with VL/SV/SVTV and using FGL. Setting up
AIG transforms is recommended especially for slow cases.
-
:skip-svex-simplify should be nil or t, and it is nil default. It tells the
program to skip svex-simplify stage. This is worthwhile to try in
case sanity-check fails.
-
:export-to-svexl should be nil or a name for a constant. It exports an ACL2
constant containing an svexl object after all the svex simplifications.
