• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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-res-rewrite-pat
            • Vl-res-rewrite-occ
          • Vl-add-res-modules
          • Vl-make-res-occs
        • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-res-rewrite-occs

Vl-res-rewrite-occ

Rewrite an occurrence to eliminate multiple drivers.

Definitions and Theorems

Function: vl-res-rewrite-occ

(defun vl-res-rewrite-occ (occ mds idx sigma)
  "Returns (MV OCC' IDX' SIGMA')"
  (declare (xargs :guard (and (natp idx)
                              (vl-emodwirelist-p (alist-keys mds))
                              (vl-res-sigma-p sigma))))
  (b* ((o (gpl :o occ))
       ((mv o idx sigma)
        (vl-res-rewrite-pat o mds idx sigma))
       (occ (acl2::chgpl :o o occ)))
    (mv occ idx sigma)))

Theorem: vl-res-rewrite-occ-mvtypes-1

(defthm vl-res-rewrite-occ-mvtypes-1
  (natp (mv-nth 1
                (vl-res-rewrite-occ occ mds idx sigma)))
  :rule-classes :type-prescription)

Theorem: vl-res-sigma-p-of-vl-res-rewrite-occ

(defthm vl-res-sigma-p-of-vl-res-rewrite-occ
 (implies
  (and (vl-emodwirelist-p (alist-keys mds))
       (vl-res-sigma-p sigma))
  (vl-res-sigma-p (mv-nth 2
                          (vl-res-rewrite-occ occ mds idx sigma)))))

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

(defthm good-esim-occp-of-vl-res-rewrite-occ
 (implies
  (good-esim-occp occ)
  (good-esim-occp (mv-nth 0
                          (vl-res-rewrite-occ occ mds idx sigma)))))