		Search-engine friendly clone of the ACL2 documentation.

Udp-elim

Vl-udp-to-module

Convert a UDP into a module.

Signature
(vl-udp-to-module x) → mod
Arguments: x — Guard (vl-udp-p x).
Returns: mod — Type (vl-module-p mod).

We always produce a new module. If the UDP is not something we can support, the resulting module will have fatal warnings.

Definitions and Theorems

Function: vl-udp-to-module

(defun vl-udp-to-module (x)
 (declare (xargs :guard (vl-udp-p x)))
 (let ((__function__ 'vl-udp-to-module))
  (declare (ignorable __function__))
  (b* (((vl-udp x))
       (portdecls (cons x.output x.inputs))
       (ports (vl-ports-from-portdecls portdecls))
       (vardecls (vl-udp-vardecls-from-portdecls portdecls))
       (atts (cons (list "VL_CONVERTED_UDP") x.atts))
       (warnings x.warnings)
       (warnings
            (if x.sequentialp
                (fatal :type :vl-sequential-udp
                       :msg "Sequential UDPs are not yet supported."
                       :args nil)
              warnings))
       ((mv ?okp warnings assigns)
        (if x.sequentialp (mv nil warnings nil)
          (vl-combinational-udptable-synth
               x.output
               x.inputs x.maxloc x.table warnings))))
    (make-vl-module :name x.name
                    :origname x.name
                    :minloc x.minloc
                    :maxloc x.maxloc
                    :comments x.comments
                    :ports ports
                    :portdecls portdecls
                    :vardecls vardecls
                    :warnings warnings
                    :assigns assigns
                    :atts atts))))

Theorem: vl-module-p-of-vl-udp-to-module

(defthm vl-module-p-of-vl-udp-to-module
  (b* ((mod (vl-udp-to-module x)))
    (vl-module-p mod))
  :rule-classes :rewrite)