• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
        • Svtv-data
          • Defsvtv$
          • Defcycle
          • Def-pipeline-thm
          • Def-svtv-data-export
          • Def-svtv-data-import
          • Svtv-name-lhs-map
            • Svtv-name-lhs-map-fix
            • Svtv-name-lhs-map-p
            • Svtv-namemap->lhsmap
            • Svtv-name-lhs-map-equiv
            • Svtv-namemap
          • Def-cycle-thm
          • Def-svtv-data-export/import
          • Defsvtv$-phasewise
        • Defsvtv$
        • Svtv-run
        • Defsvtv-phasewise
        • Svtv
        • Svtv-spec
        • Defsvtv
        • Process.lisp
        • Svtv-doc
        • Svtv-chase$
        • Svtv-versus-stv
        • Svtv-debug-fsm
        • Structure.lisp
        • Svtv-debug
        • Def-pipeline-thm
        • Expand.lisp
        • Def-cycle-thm
        • Svtv-utilities
        • Svtv-debug$
        • Defsvtv$-phasewise
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svtv-name-lhs-map

Svtv-namemap->lhsmap

Processes a list of nicknames for SystemVerilog-syntax signals into an internal form.

Signature

(svtv-namemap->lhsmap x modidx moddb aliases) 
  → 
(mv errs lhses)

Arguments

x — User-provided mapping. An alist where the keys are arbitary names (svars, typically symbols) and the values are SystemVerilog-syntax hierarchical names (strings).
    Guard (svtv-namemap-p x).

modidx — Guard (natp modidx).

moddb — Guard (moddb-ok moddb).

Returns

lhses — Type (svtv-name-lhs-map-p lhses).

Definitions and Theorems

Function: svtv-namemap->lhsmap

(defun svtv-namemap->lhsmap (x modidx moddb aliases)
  (declare (xargs :stobjs (moddb aliases)))
  (declare (xargs :guard (and (svtv-namemap-p x)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare
       (xargs :guard (svtv-mod-alias-guard modidx moddb aliases)))
  (let ((__function__ 'svtv-namemap->lhsmap))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil nil))
         ((unless (mbt (and (consp (car x))
                            (svar-p (caar x)))))
          (svtv-namemap->lhsmap (cdr x)
                                modidx moddb aliases))
         ((mv err1 first)
          (svtv-wire->lhs! (cdar x)
                           modidx moddb aliases))
         ((mv errs rest)
          (svtv-namemap->lhsmap (cdr x)
                                modidx moddb aliases))
         ((when err1)
          (mv (append-without-guard err1 errs)
              rest)))
      (mv errs
          (cons (cons (caar x) first) rest)))))

Theorem: svtv-name-lhs-map-p-of-svtv-namemap->lhsmap.lhses

(defthm svtv-name-lhs-map-p-of-svtv-namemap->lhsmap.lhses
  (b* (((mv ?errs ?lhses)
        (svtv-namemap->lhsmap x modidx moddb aliases)))
    (svtv-name-lhs-map-p lhses))
  :rule-classes :rewrite)

Theorem: svtv-namemap->lhsmap-of-svtv-namemap-fix-x

(defthm svtv-namemap->lhsmap-of-svtv-namemap-fix-x
  (equal (svtv-namemap->lhsmap (svtv-namemap-fix x)
                               modidx moddb aliases)
         (svtv-namemap->lhsmap x modidx moddb aliases)))

Theorem: svtv-namemap->lhsmap-svtv-namemap-equiv-congruence-on-x

(defthm svtv-namemap->lhsmap-svtv-namemap-equiv-congruence-on-x
  (implies
       (svtv-namemap-equiv x x-equiv)
       (equal (svtv-namemap->lhsmap x modidx moddb aliases)
              (svtv-namemap->lhsmap x-equiv modidx moddb aliases)))
  :rule-classes :congruence)

Theorem: svtv-namemap->lhsmap-of-nfix-modidx

(defthm svtv-namemap->lhsmap-of-nfix-modidx
  (equal (svtv-namemap->lhsmap x (nfix modidx)
                               moddb aliases)
         (svtv-namemap->lhsmap x modidx moddb aliases)))

Theorem: svtv-namemap->lhsmap-nat-equiv-congruence-on-modidx

(defthm svtv-namemap->lhsmap-nat-equiv-congruence-on-modidx
  (implies
       (nat-equiv modidx modidx-equiv)
       (equal (svtv-namemap->lhsmap x modidx moddb aliases)
              (svtv-namemap->lhsmap x modidx-equiv moddb aliases)))
  :rule-classes :congruence)

Theorem: svtv-namemap->lhsmap-of-moddb-fix-moddb

(defthm svtv-namemap->lhsmap-of-moddb-fix-moddb
  (equal (svtv-namemap->lhsmap x modidx (moddb-fix moddb)
                               aliases)
         (svtv-namemap->lhsmap x modidx moddb aliases)))

Theorem: svtv-namemap->lhsmap-moddb-equiv-congruence-on-moddb

(defthm svtv-namemap->lhsmap-moddb-equiv-congruence-on-moddb
  (implies
       (moddb-equiv moddb moddb-equiv)
       (equal (svtv-namemap->lhsmap x modidx moddb aliases)
              (svtv-namemap->lhsmap x modidx moddb-equiv aliases)))
  :rule-classes :congruence)

Theorem: svtv-namemap->lhsmap-of-lhslist-fix-aliases

(defthm svtv-namemap->lhsmap-of-lhslist-fix-aliases
  (equal (svtv-namemap->lhsmap x modidx moddb (lhslist-fix aliases))
         (svtv-namemap->lhsmap x modidx moddb aliases)))

Theorem: svtv-namemap->lhsmap-lhslist-equiv-congruence-on-aliases

(defthm svtv-namemap->lhsmap-lhslist-equiv-congruence-on-aliases
  (implies
       (lhslist-equiv aliases aliases-equiv)
       (equal (svtv-namemap->lhsmap x modidx moddb aliases)
              (svtv-namemap->lhsmap x modidx moddb aliases-equiv)))
  :rule-classes :congruence)