• 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-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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-res-rewrite-occs

Vl-res-rewrite-pat

Rewrite an output pattern to eliminate multiple drivers.

Signature: (vl-res-rewrite-pat pat mds idx sigma) returns (mv pat' idx' sigma').

PAT should be the output pattern for some occurrence, e.g., (gpl :o occ). The other arguments are as in vl-res-rewrite-occs.

We replace any multiply driven wires with new, freshly generated names, and update IDX and SIGMA appropriately to account for the newly generated names.

Definitions and Theorems

Function: vl-res-rewrite-pat

(defun vl-res-rewrite-pat (pat mds idx sigma)
  "Returns (MV PAT' IDX' SIGMA')"
  (declare (xargs :guard (and (natp idx)
                              (vl-emodwirelist-p (alist-keys mds))
                              (vl-res-sigma-p sigma))))
  (b* ((idx (lnfix idx))
       ((when (not pat)) (mv pat idx sigma))
       ((when (atom pat))
        (b* ((look (hons-get pat mds))
             ((unless look) (mv pat idx sigma))
             (idx (+ 1 idx))
             (fresh (make-vl-emodwire :basename "vl_res"
                                      :index idx))
             (prev (cdr (hons-get pat sigma)))
             (sigma (hons-acons pat (cons fresh prev)
                                sigma)))
          (mv fresh idx sigma)))
       ((mv car idx sigma)
        (vl-res-rewrite-pat (car pat)
                            mds idx sigma))
       ((mv cdr idx sigma)
        (vl-res-rewrite-pat (cdr pat)
                            mds idx sigma)))
    (mv (cons car cdr) idx sigma)))

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

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

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

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

Theorem: similar-patternsp-of-vl-res-rewrite-pat

(defthm similar-patternsp-of-vl-res-rewrite-pat
  (similar-patternsp (mv-nth 0
                             (vl-res-rewrite-pat pat mds idx sigma))
                     pat))