		Search-engine friendly clone of the ACL2 documentation.

Svl-flatten-design

Generate SVL designs from SV and VL Designs

Signature
(svl-flatten-design sv-design vl-design &key (rp-state 'rp-state) (dont-flatten 'nil) (top 'nil) (state 'state)) → (mv * rp-state)
Arguments: sv-design — Guard (sv::design-p sv-design).

Using SV and VL (to determine the size of the module inputs only) designs, creates an SVL design.


(svl-flatten-design sv-design
                    vl-design
                    :dont-flatten ...
                    :top ...)

The sv-design and vl-design arguments are mandatory sv::sv-tutorial.

The SVL system allows some of the modules to be flattened, and some untouched to remain circuit hierarchy

:dont-flatten List of names of the modules that should not be flattened. They should be the original names of the modules from the original Verilog designs, but not from SV designs. If users want to not flatten all of the modules, they can pass :all. By default, this value is set to nil, which tells the system to flatten all the modules.

:top By default, this is set to nil. It tells the program to get the top module name from SV Design, if the users want to select another module as top, then they can provide the name of that module here. Then, only that module and its submodules will be processed. If you pass a module name in dont-flatten that is not a submodule of top, that module will be processed anyway as well.

:rp-state and :state are STOBJs. Users do not need to make assignments to them.

Definitions and Theorems

Function: svl-flatten-design-fn

(defun acl2::svl-flatten-design-fn
       (sv-design vl-design
                  rp-state dont-flatten top state)
 (declare (xargs :stobjs (rp-state state)))
 (declare (xargs :guard (sv::design-p sv-design)))
 (declare (xargs :guard (and (or (not top) (stringp top))
                             (or (equal dont-flatten :all)
                                 (string-listp dont-flatten)))))
 (let ((acl2::__function__ 'svl-flatten-design))
  (declare (ignorable acl2::__function__))
  (b*
   (((sv::design sv-design) sv-design)
    (sv-design.modalist
         (true-list-fix (make-fast-alist sv-design.modalist)))
    (all-modnames
         (get-string-modnames (strip-cars sv-design.modalist)))
    (dont-flatten-all (equal dont-flatten ':all))
    (top
     (if top top
      (progn$ (if (stringp sv-design.top)
                  sv-design.top
                (or (hard-error 'svl-flatten-design
                                "sv-design.top name is not string~%"
                                nil)
                    "")))))
    (dont-flatten
         (if dont-flatten-all
             (get-sv-submodules top sv-design.modalist nil)
           (fix-dont-flatten (union-equal dont-flatten (list top))
                             all-modnames)))
    (vl-insouts (vl-design-to-insouts-wrapper
                     vl-design sv-design dont-flatten state))
    (dont-flatten (if dont-flatten-all dont-flatten
                    (clean-dont-flatten dont-flatten all-modnames)))
    (vl-insouts (vl-insouts-insert-wire-sizes
                     vl-insouts sv-design dont-flatten))
    (rp-state (rp::rp-state-new-run rp-state))
    (rp-state (rp::rp-state-init-rules (svex-simplify-rules-fn)
                                       nil nil rp-state state))
    (- (rp::check-if-clause-processor-up-to-date (w state)))
    (-
     (cw "Starting to flatten modules and create SVL design... ~%"))
    ((mv modules rp-state)
     (svl-flatten-mods dont-flatten sv-design.modalist
                       dont-flatten vl-insouts))
    (- (hons-clear t))
    (- (cw "Inserting ranks to unflattened modules... ~%"))
    (ranks
         (svl-mod-calculate-ranks top modules nil nil (expt 2 30)))
    (modules (update-modules-with-ranks ranks modules))
    (- (cw "All done! ~%"))
    (- (fast-alist-free sv-design.modalist)))
   (mv modules rp-state))))