• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
        • Esim-primitives
        • E-conversion
          • Vl-ealist-p
          • Modinsts-to-eoccs
          • Vl-module-make-esim
          • Exploding-vectors
          • Resolving-multiple-drivers
            • Vl-res-sigma-p
            • Vl-res-rewrite-occs
            • Vl-add-res-modules
            • Vl-make-res-occs
              • Vl-make-n-bit-res-module
              • Vl-make-res-sexpr
              • Vl-make-res-occ
            • Vl-modulelist-make-esims
            • Vl-module-check-e-ok
            • Vl-collect-design-wires
            • Adding-z-drivers
            • Vl-design-to-e
            • Vl-design-to-e-check-ports
            • Vl-design-to-e-main
            • Port-bit-checking
          • Esim-steps
          • Patterns
          • Mod-internal-paths
          • Defmodules
          • Esim-simplify-update-fns
          • Esim-tutorial
          • Esim-vl
        • Vl2014
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-make-res-occs

    Vl-make-res-occ

    Generate and instantiate an appropriate resolution module to drive a wire to multiple values.

    (vl-make-res-occ name out ins) builds an E occurrence that simultaneously drives out to all of the values on ins.

    Definitions and Theorems

    Function: vl-make-res-occ

    (defun vl-make-res-occ (name out ins)
      (declare (xargs :guard (and (vl-emodwire-p out)
                                  (vl-emodwirelist-p ins)
                                  (true-listp ins)
                                  (uniquep ins))))
      (b* ((n (len ins))
           (op (vl-make-n-bit-res-module n))
           (i (and (posp n) (list ins)))
           (o (list (list out))))
        (list :u name :op op :i i :o o)))

    Theorem: good-esim-occp-of-vl-make-res-occ

    (defthm good-esim-occp-of-vl-make-res-occ
      (implies (and (force (vl-emodwire-p out))
                    (force (vl-emodwirelist-p ins))
                    (force (true-listp ins))
                    (force (uniquep ins))
                    (force name))
               (good-esim-occp (vl-make-res-occ name out ins))))