• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
          • Basic-bind-elim
          • Argresolve
          • Basicsanity
          • Portdecl-sign
          • Enum-names
          • Port-resolve
          • Udp-elim
            • Vl-udp-vardecls-from-portdecls
            • Vl-udps-to-modules
            • Vl-udpline-match-expr
            • Vl-combinational-udptable-synth
            • Vl-udptable-assignrhs
            • Vl-udp-to-module
            • Vl-udp-vardecl-from-portdecl
            • Vl-design-udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• 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 (list* (list "VL_CONVERTED_UDP")
                    (if x.sequentialp (list "VL_SEQUENTIAL_UDP")
                        (list "VL_COMBINATIONAL_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)