		Search-engine friendly clone of the ACL2 documentation.

Cblock-path-checking

Vl-module-combinational-elim

Signature
(vl-module-combinational-elim x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Type (vl-module-p new-x), given the guard.

Definitions and Theorems

Function: vl-module-combinational-elim

(defun vl-module-combinational-elim (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-combinational-elim))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    ((when (vl-module->hands-offp x)) x)
    ((unless x.alwayses) x)
    ((when x.initials)
     (b*
      ((w
        (make-vl-warning
         :type :vl-programming-error
         :msg
         "Trying to eliminate combinational always blocks, but ~
                       the module still has initial blocks?  You should have ~
                       run eliminitial first."
         :args nil
         :fatalp nil
         :fn __function__)))
      (change-vl-module x
                        :warnings (cons w x.warnings))))
    (warnings x.warnings)
    (scary (vl-always-scary-regs x.alwayses))
    ((mv cblocks ?others warnings)
     (vl-filter-cblocks x.alwayses x.vardecls scary warnings))
    ((unless cblocks)
     (change-vl-module x :warnings warnings))
    (delta (vl-starting-delta x))
    (delta (change-vl-delta delta
                            :assigns x.assigns))
    ((mv delta cvtregs)
     (vl-cblocks-synth cblocks x.vardecls delta))
    ((vl-delta delta) delta)
    ((mv fixed-vardecls fixed-portdecls)
     (vl-convert-regs cvtregs x.vardecls x.portdecls))
    (final-vardecls
         (append-without-guard fixed-vardecls delta.vardecls))
    ((unless (uniquep (vl-vardecllist->names final-vardecls)))
     (raise
        "Name clash when converting combinational blocks!  ~x0."
        (duplicated-members (vl-vardecllist->names final-vardecls)))
     x)
    (new-x (change-vl-module x
                             :alwayses others
                             :vardecls final-vardecls
                             :portdecls fixed-portdecls
                             :assigns delta.assigns
                             :warnings delta.warnings)))
   new-x)))

Theorem: vl-module-p-of-vl-module-combinational-elim

(defthm vl-module-p-of-vl-module-combinational-elim
  (implies (and (force (vl-module-p x)))
           (b* ((new-x (vl-module-combinational-elim x)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)