		Search-engine friendly clone of the ACL2 documentation.

Udp-elim

Vl-combinational-udptable-synth

Translate a combinational UDP table into an assignment.

Signature
(vl-combinational-udptable-synth output inputs loc x warnings) → (mv okp warnings assigns)
Arguments: output — Guard (vl-portdecl-p output).; inputs — Guard (vl-portdecllist-p inputs).; loc — Guard (vl-location-p loc).; x — Guard (vl-udptable-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: okp — Type (booleanp okp).; warnings — Type (vl-warninglist-p warnings).; assigns — Type (vl-assignlist-p assigns).

Definitions and Theorems

Function: vl-combinational-udptable-synth

(defun vl-combinational-udptable-synth
       (output inputs loc x warnings)
  (declare (xargs :guard (and (vl-portdecl-p output)
                              (vl-portdecllist-p inputs)
                              (vl-location-p loc)
                              (vl-udptable-p x)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-combinational-udptable-synth))
    (declare (ignorable __function__))
    (b* ((outname (vl-portdecl->name output))
         (outexpr (vl-idexpr outname nil nil))
         (innames (vl-portdecllist->names inputs))
         (inexprs (vl-make-idexpr-list innames nil nil))
         ((unless (consp inexprs))
          (mv nil
              (fatal :type :vl-bad-udp
                     :msg "UDP has no inputs?")
              nil))
         ((mv okp warnings rhs)
          (vl-udptable-assignrhs inexprs x warnings))
         ((unless okp) (mv nil warnings nil))
         (assign (make-vl-assign :lvalue outexpr
                                 :expr rhs
                                 :loc loc)))
      (mv t (ok) (list assign)))))

Theorem: booleanp-of-vl-combinational-udptable-synth.okp

(defthm booleanp-of-vl-combinational-udptable-synth.okp
 (b*
  (((mv ?okp ?warnings ?assigns)
    (vl-combinational-udptable-synth output inputs loc x warnings)))
  (booleanp okp))
 :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-combinational-udptable-synth.warnings

(defthm vl-warninglist-p-of-vl-combinational-udptable-synth.warnings
 (b*
  (((mv ?okp ?warnings ?assigns)
    (vl-combinational-udptable-synth output inputs loc x warnings)))
  (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-assignlist-p-of-vl-combinational-udptable-synth.assigns

(defthm vl-assignlist-p-of-vl-combinational-udptable-synth.assigns
 (b*
  (((mv ?okp ?warnings ?assigns)
    (vl-combinational-udptable-synth output inputs loc x warnings)))
  (vl-assignlist-p assigns))
 :rule-classes :rewrite)