• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
        • Def-svtv-generalized-thm
        • Override-transparent
        • Def-svtv-to-fsm-thm
        • Svtv-decomposition-choosing-a-method
        • Def-svtv-refinement
        • Def-svtv-ideal
          • Svtv-idealize-internals
            • Svtv-override-triplemap-key-check
        • Def-override-transparent
      • 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

• Svtv-idealize-internals

Svtv-override-triplemap-key-check

Checks that the given key either isn't bound the test alist, or else has a triple in the triplemap such that the test of the triple is the key's binding in the test-alist, the val of the triple is the key's binding in the val-alist, and the refvar of the triple is bound in probes to a probe whose signal is the key and time is the current phase.

Signature

(svtv-override-triplemap-key-check 
     key phase 
     test-alist val-alist probes triplemap) 
 
  → 
ok

Arguments

key — Guard (svar-p key).

phase — Guard (natp phase).

test-alist — Guard (svex-alist-p test-alist).

val-alist — Guard (svex-alist-p val-alist).

probes — Guard (svtv-probealist-p probes).

triplemap — Guard (svtv-override-triplemap-p triplemap).

Definitions and Theorems

Function: svtv-override-triplemap-key-check

(defun svtv-override-triplemap-key-check
       (key phase
            test-alist val-alist probes triplemap)
 (declare
      (xargs :guard (and (svar-p key)
                         (natp phase)
                         (svex-alist-p test-alist)
                         (svex-alist-p val-alist)
                         (svtv-probealist-p probes)
                         (svtv-override-triplemap-p triplemap))))
 (let ((__function__ 'svtv-override-triplemap-key-check))
   (declare (ignorable __function__))
   (b*
     ((test (svex-fastlookup key test-alist))
      ((unless test) t)
      (val (or (svex-fastlookup key val-alist)
               (svex-x)))
      (triple
           (cdr (hons-get (svar-fix key)
                          (svtv-override-triplemap-fix triplemap))))
      ((unless triple) nil)
      ((svtv-override-triple triple))
      ((unless (and (equal triple.test test)
                    (equal triple.val val)))
       nil)
      ((unless triple.refvar) t)
      (probe (cdr (hons-get triple.refvar
                            (svtv-probealist-fix probes))))
      ((unless probe) nil)
      ((svtv-probe probe)))
     (and (equal probe.signal (svar-fix key))
          (equal probe.time (lnfix phase))))))

Theorem: svtv-override-triplemap-key-check-implies-4vec-override-mux-<<=

(defthm
    svtv-override-triplemap-key-check-implies-4vec-override-mux-<<=
  (b* ((vl::?ok (svtv-override-triplemap-key-check
                     key phase
                     test-alist val-alist probes triplemap)))
    (implies (and ok
                  (svtv-override-triple-envs-ok
                       (cdr (hons-assoc-equal (svar-fix key)
                                              triplemap))
                       pipe-env spec-env
                       (svtv-probealist-extract probes ref-envs)))
             (4vec-override-mux-<<=
                  (svex-eval (svex-lookup key test-alist)
                             pipe-env)
                  (svex-eval (svex-lookup key val-alist)
                             pipe-env)
                  (svex-eval (svex-lookup key test-alist)
                             spec-env)
                  (svex-eval (svex-lookup key val-alist)
                             spec-env)
                  (svex-env-lookup key (nth phase ref-envs))))))

Theorem: svtv-override-triplemap-key-check-implies-4vec-muxtest-subsetp

(defthm
     svtv-override-triplemap-key-check-implies-4vec-muxtest-subsetp
 (b* ((vl::?ok (svtv-override-triplemap-key-check
                    key phase
                    test-alist val-alist probes triplemap)))
  (implies
       (and ok
            (svtv-override-triple-envs-ok
                 (cdr (hons-assoc-equal (svar-fix key)
                                        triplemap))
                 pipe-env spec-env ref-env))
       (4vec-muxtest-subsetp (svex-eval (svex-lookup key test-alist)
                                        spec-env)
                             (svex-eval (svex-lookup key test-alist)
                                        pipe-env)))))

Theorem: svtv-override-triplemap-key-check-implies-lookup-in-triplemap

(defthm
      svtv-override-triplemap-key-check-implies-lookup-in-triplemap
  (b* ((vl::?ok (svtv-override-triplemap-key-check
                     key phase
                     test-alist val-alist probes triplemap)))
    (implies (and ok
                  (case-split (svex-lookup key test-alist)))
             (hons-assoc-equal (svar-fix key)
                               triplemap))))

Theorem: svtv-override-triplemap-key-check-of-svar-fix-key

(defthm svtv-override-triplemap-key-check-of-svar-fix-key
  (equal (svtv-override-triplemap-key-check
              (svar-fix key)
              phase
              test-alist val-alist probes triplemap)
         (svtv-override-triplemap-key-check
              key phase
              test-alist val-alist probes triplemap)))

Theorem: svtv-override-triplemap-key-check-svar-equiv-congruence-on-key

(defthm
     svtv-override-triplemap-key-check-svar-equiv-congruence-on-key
  (implies (svar-equiv key key-equiv)
           (equal (svtv-override-triplemap-key-check
                       key phase
                       test-alist val-alist probes triplemap)
                  (svtv-override-triplemap-key-check
                       key-equiv phase
                       test-alist val-alist probes triplemap)))
  :rule-classes :congruence)

Theorem: svtv-override-triplemap-key-check-of-nfix-phase

(defthm svtv-override-triplemap-key-check-of-nfix-phase
  (equal (svtv-override-triplemap-key-check
              key (nfix phase)
              test-alist val-alist probes triplemap)
         (svtv-override-triplemap-key-check
              key phase
              test-alist val-alist probes triplemap)))

Theorem: svtv-override-triplemap-key-check-nat-equiv-congruence-on-phase

(defthm
    svtv-override-triplemap-key-check-nat-equiv-congruence-on-phase
  (implies (nat-equiv phase phase-equiv)
           (equal (svtv-override-triplemap-key-check
                       key phase
                       test-alist val-alist probes triplemap)
                  (svtv-override-triplemap-key-check
                       key phase-equiv
                       test-alist val-alist probes triplemap)))
  :rule-classes :congruence)

Theorem: svtv-override-triplemap-key-check-of-svex-alist-fix-test-alist

(defthm
     svtv-override-triplemap-key-check-of-svex-alist-fix-test-alist
  (equal (svtv-override-triplemap-key-check
              key phase (svex-alist-fix test-alist)
              val-alist probes triplemap)
         (svtv-override-triplemap-key-check
              key phase
              test-alist val-alist probes triplemap)))

Theorem: svtv-override-triplemap-key-check-svex-alist-equiv-congruence-on-test-alist

(defthm
 svtv-override-triplemap-key-check-svex-alist-equiv-congruence-on-test-alist
 (implies
  (svex-alist-equiv test-alist test-alist-equiv)
  (equal
    (svtv-override-triplemap-key-check
         key phase
         test-alist val-alist probes triplemap)
    (svtv-override-triplemap-key-check key phase test-alist-equiv
                                       val-alist probes triplemap)))
 :rule-classes :congruence)

Theorem: svtv-override-triplemap-key-check-of-svex-alist-fix-val-alist

(defthm
      svtv-override-triplemap-key-check-of-svex-alist-fix-val-alist
  (equal (svtv-override-triplemap-key-check
              key phase
              test-alist (svex-alist-fix val-alist)
              probes triplemap)
         (svtv-override-triplemap-key-check
              key phase
              test-alist val-alist probes triplemap)))

Theorem: svtv-override-triplemap-key-check-svex-alist-equiv-congruence-on-val-alist

(defthm
 svtv-override-triplemap-key-check-svex-alist-equiv-congruence-on-val-alist
 (implies (svex-alist-equiv val-alist val-alist-equiv)
          (equal (svtv-override-triplemap-key-check
                      key phase
                      test-alist val-alist probes triplemap)
                 (svtv-override-triplemap-key-check
                      key phase test-alist
                      val-alist-equiv probes triplemap)))
 :rule-classes :congruence)

Theorem: svtv-override-triplemap-key-check-of-svtv-probealist-fix-probes

(defthm
    svtv-override-triplemap-key-check-of-svtv-probealist-fix-probes
  (equal (svtv-override-triplemap-key-check
              key phase test-alist
              val-alist (svtv-probealist-fix probes)
              triplemap)
         (svtv-override-triplemap-key-check
              key phase
              test-alist val-alist probes triplemap)))

Theorem: svtv-override-triplemap-key-check-svtv-probealist-equiv-congruence-on-probes

(defthm
 svtv-override-triplemap-key-check-svtv-probealist-equiv-congruence-on-probes
 (implies (svtv-probealist-equiv probes probes-equiv)
          (equal (svtv-override-triplemap-key-check
                      key phase
                      test-alist val-alist probes triplemap)
                 (svtv-override-triplemap-key-check
                      key phase test-alist
                      val-alist probes-equiv triplemap)))
 :rule-classes :congruence)

Theorem: svtv-override-triplemap-key-check-of-svtv-override-triplemap-fix-triplemap

(defthm
 svtv-override-triplemap-key-check-of-svtv-override-triplemap-fix-triplemap
 (equal (svtv-override-triplemap-key-check
             key phase test-alist val-alist probes
             (svtv-override-triplemap-fix triplemap))
        (svtv-override-triplemap-key-check
             key phase
             test-alist val-alist probes triplemap)))

Theorem: svtv-override-triplemap-key-check-svtv-override-triplemap-equiv-congruence-on-triplemap

(defthm
 svtv-override-triplemap-key-check-svtv-override-triplemap-equiv-congruence-on-triplemap
 (implies (svtv-override-triplemap-equiv triplemap triplemap-equiv)
          (equal (svtv-override-triplemap-key-check
                      key phase
                      test-alist val-alist probes triplemap)
                 (svtv-override-triplemap-key-check
                      key phase test-alist
                      val-alist probes triplemap-equiv)))
 :rule-classes :congruence)