• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
        • Svtv-data
        • Defsvtv$
        • Svtv-run
        • Defsvtv-phasewise
        • Svtv
        • Svtv-spec
        • Defsvtv
        • Process.lisp
          • Svtv-compile
          • Defsvtv-events
          • Svtv-compile-lazy
          • Svtv-compile-phase
          • Svtv-compile-phases-lazy
          • Svtv-allphases-inputs
          • Svtv-phase-inputs
          • Svtv-inalist-resolve-unassigned
          • Svtv-simplify-outs/states
          • Svtv-collect-inmap
          • Svar-boolmasks-limit-to-bound-vars
          • Svtv-overrides->assigns
          • Svtv-non-override-test-input-vars
          • Svtv-outputs->outalist
          • Svtv-run-squash-dontcares
          • Svtv-inputs->assigns
          • Svtv-phase-var-assigns
          • Defsvtv-fn
          • Svtv-entries->overrideconds
          • Svtv-entries->vars
          • Svtv-easy-bindings-main
          • Svtv-collect-masks
          • Svtv-baseentry-svex
          • Svtv-init-states
          • Lhs->mask
          • Svtv-easy-bindings-svtv-vars
          • Svtv-autoins-aux
          • Svtv-autohyps-aux
          • Svtv-autobinds-aux
          • Svtv-autoins
          • Svtv-autohyps
          • Svtv-autobinds
          • Fast-alist-free-list
          • Defsvtv-default-names
        • 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Process.lisp

Svtv-non-override-test-input-vars

Signature

(svtv-non-override-test-input-vars x map) → new-x

Arguments

x — Guard (svarlist-p x).

map — Guard (svtv-inputmap-p map).

Returns

new-x — Type (svarlist-p new-x).

Definitions and Theorems

Function: svtv-non-override-test-input-vars

(defun svtv-non-override-test-input-vars (x map)
  (declare (xargs :guard (and (svarlist-p x)
                              (svtv-inputmap-p map))))
  (let ((__function__ 'svtv-non-override-test-input-vars))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (eq (cdr (hons-get (svar-fix (car x))
                             (svtv-inputmap-fix map)))
              :override-test)
          (svtv-non-override-test-input-vars (cdr x)
                                             map)
        (cons (svar-fix (car x))
              (svtv-non-override-test-input-vars (cdr x)
                                                 map))))))

Theorem: svarlist-p-of-svtv-non-override-test-input-vars

(defthm svarlist-p-of-svtv-non-override-test-input-vars
  (b* ((new-x (svtv-non-override-test-input-vars x map)))
    (svarlist-p new-x))
  :rule-classes :rewrite)

Theorem: svtv-non-override-test-input-vars-of-svarlist-fix-x

(defthm svtv-non-override-test-input-vars-of-svarlist-fix-x
  (equal (svtv-non-override-test-input-vars (svarlist-fix x)
                                            map)
         (svtv-non-override-test-input-vars x map)))

Theorem: svtv-non-override-test-input-vars-svarlist-equiv-congruence-on-x

(defthm
   svtv-non-override-test-input-vars-svarlist-equiv-congruence-on-x
  (implies (svarlist-equiv x x-equiv)
           (equal (svtv-non-override-test-input-vars x map)
                  (svtv-non-override-test-input-vars x-equiv map)))
  :rule-classes :congruence)

Theorem: svtv-non-override-test-input-vars-of-svtv-inputmap-fix-map

(defthm svtv-non-override-test-input-vars-of-svtv-inputmap-fix-map
  (equal
       (svtv-non-override-test-input-vars x (svtv-inputmap-fix map))
       (svtv-non-override-test-input-vars x map)))

Theorem: svtv-non-override-test-input-vars-svtv-inputmap-equiv-congruence-on-map

(defthm
 svtv-non-override-test-input-vars-svtv-inputmap-equiv-congruence-on-map
 (implies (svtv-inputmap-equiv map map-equiv)
          (equal (svtv-non-override-test-input-vars x map)
                 (svtv-non-override-test-input-vars x map-equiv)))
 :rule-classes :congruence)