|
|
|---|
|
|
|
|---|
Convert an SVL design to an sv::svex-alist.
Using ACL2::rp-rewriter, converts an SVL design usign svl-run to an sv::svex-alist.
(svl-run->svex-alist :modname <modname> :svl-design <svl-design> :binds-ins-alist <binds-ins-alist> :binds-out-alist <binds-out-alist> :svex-alist-name <svex-alist-name> :rw-rule-name <rw-rule-name>)
Users should provide a value for all the keys.
modname: name of the main module in an SVL design.
svl-design: SVL design constant.
binds-ins-alist: Input simulation pattern constant similar to inputs key of defsvtv.
binds-out-alist: Output simulation pattern constant similar to outputs key of defsvtv.
svex-alist-name: when the SVL-design is converted to an svex-alist, the program will create a constant provided by svex-alist-name.
rw-rule-name: the program also creates a rewrite rule with this given name. The LHS of this rewrite rule is svl-run of the given module with given configuration, and the RHS is svex-alist-eval of the newly generated svex-alist.
The keys in created svex-alist are the variables designated in binds-out-alist. The variables in the values (svexes) share the same name as the variables from binds-ins-alist.
An example call to svl-run-compose is given below. It submits an event that exports svl-run-top-module-composed and *svl-run-top-module-composed*.
(svl-run->svex-alist :modname "top_module" :binds-ins-alist *ins-alist* :binds-out-alist *outs-alist* :svl-design *svl-netlist* :rw-rule-name svl-run-top-module-composed :svex-alist-name *svl-run-top-module-composed*)
This will produce a constant *svl-run-top-module-composed*, which has the svex-alist representation of the given svl-run instance; and a rewrite rule with the name svl-run-top-module-composed, which rewrites the svl-run instance to evaluation of this svex-alist. See svl-run for concrete examples of the first four keys (:modname, :binds-ins-alist, :binds-out-alist, :svl-design).