• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
        • Def-svtv-generalized-thm
          • Svtv-override-triplemaplist-envs-match
        • Override-transparent
        • Def-svtv-to-fsm-thm
        • Svtv-decomposition-choosing-a-method
        • Def-svtv-refinement
        • Def-svtv-ideal
        • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Def-svtv-generalized-thm

Svtv-override-triplemaplist-envs-match

Checks that the given environment env has values matching spec for the override test and value variables of the given triplemaplist triplemaps.

Signature

(svtv-override-triplemaplist-envs-match triplemaps env spec) 
  → 
*

Arguments

triplemaps — Guard (svtv-override-triplemaplist-p triplemaps).

env — Guard (svex-env-p env).

spec — Guard (svex-env-p spec).

An occurrence of this function is used by def-svtv-generalized-thm as a hypothesis of the generalized theorems it proves, serving to assume that the environment used in the SVTV run of the theorem overrides exactly the signals it's supposed to, i.e. matching spec.

This function returns true iff for every svtv-override-triple in triplemaps, the evaluation of the test field on env equals its evaluation on spec, and the evaluation of the val field on spec is 4vec-<<= its evaluation on env. In the current framework each test and val expression is always either a constant or variable. For constants, the conditions are automatically true, and for variables the bindings in env and spec must be compared.

When instantiating a generalized SVTV theorem (as produced by def-svtv-generalized-thm to prove something about an SVTV run on a more particular environment, there are a couple of helpful rewriting strategies.

• svtv-override-triplemaplist-envs-match-simplify applies when env is a term containing a list of pairs with constant keys and (as is usually the case) spec is a constant. It simplifies the call of svtv-override-triplemaplist-envs-match to a call of svtv-override-triplelist-envs-match on a smaller set of triples, only the ones that couldn't be resolved by just examining the syntax of the env and spec terms. Then, svtv-override-triplelist-envs-match has rules to open up and solve the requirements for the remaining triples.
• svtv-override-triplemaplist-envs-match-remove-irrelevant-pair-top can simplify env terms containing irrelevant pairs, i.e. those that aren't test or value variables of the triplemaps.

Definitions and Theorems

Function: svtv-override-triplemaplist-envs-match

(defun svtv-override-triplemaplist-envs-match (triplemaps env spec)
 (declare
      (xargs :guard (and (svtv-override-triplemaplist-p triplemaps)
                         (svex-env-p env)
                         (svex-env-p spec))))
 (let ((__function__ 'svtv-override-triplemaplist-envs-match))
  (declare (ignorable __function__))
  (mbe
    :logic
    (if (atom triplemaps)
        t
      (and (svtv-override-triplemap-envs-match (car triplemaps)
                                               env spec)
           (svtv-override-triplemaplist-envs-match (cdr triplemaps)
                                                   env spec)))
    :exec
    (with-fast-alist env
                     (with-fast-alist spec
                                      (svtv-override-triplemaplist-envs-match-aux
                                           triplemaps env spec))))))

Theorem: svtv-override-triplemaplist-envs-match-of-svtv-override-triplemaplist-fix-triplemaps

(defthm
 svtv-override-triplemaplist-envs-match-of-svtv-override-triplemaplist-fix-triplemaps
 (equal
      (svtv-override-triplemaplist-envs-match
           (svtv-override-triplemaplist-fix triplemaps)
           env spec)
      (svtv-override-triplemaplist-envs-match triplemaps env spec)))

Theorem: svtv-override-triplemaplist-envs-match-svtv-override-triplemaplist-equiv-congruence-on-triplemaps

(defthm
 svtv-override-triplemaplist-envs-match-svtv-override-triplemaplist-equiv-congruence-on-triplemaps
 (implies
   (svtv-override-triplemaplist-equiv triplemaps triplemaps-equiv)
   (equal
        (svtv-override-triplemaplist-envs-match triplemaps env spec)
        (svtv-override-triplemaplist-envs-match
             triplemaps-equiv env spec)))
 :rule-classes :congruence)

Theorem: svtv-override-triplemaplist-envs-match-of-svex-env-fix-env

(defthm svtv-override-triplemaplist-envs-match-of-svex-env-fix-env
 (equal
      (svtv-override-triplemaplist-envs-match
           triplemaps (svex-env-fix env)
           spec)
      (svtv-override-triplemaplist-envs-match triplemaps env spec)))

Theorem: svtv-override-triplemaplist-envs-match-svex-env-equiv-congruence-on-env

(defthm
 svtv-override-triplemaplist-envs-match-svex-env-equiv-congruence-on-env
 (implies
   (svex-env-equiv env env-equiv)
   (equal
        (svtv-override-triplemaplist-envs-match triplemaps env spec)
        (svtv-override-triplemaplist-envs-match
             triplemaps env-equiv spec)))
 :rule-classes :congruence)

Theorem: svtv-override-triplemaplist-envs-match-of-svex-env-fix-spec

(defthm svtv-override-triplemaplist-envs-match-of-svex-env-fix-spec
 (equal
      (svtv-override-triplemaplist-envs-match
           triplemaps env (svex-env-fix spec))
      (svtv-override-triplemaplist-envs-match triplemaps env spec)))

Theorem: svtv-override-triplemaplist-envs-match-svex-env-equiv-congruence-on-spec

(defthm
 svtv-override-triplemaplist-envs-match-svex-env-equiv-congruence-on-spec
 (implies
   (svex-env-equiv spec spec-equiv)
   (equal
        (svtv-override-triplemaplist-envs-match triplemaps env spec)
        (svtv-override-triplemaplist-envs-match
             triplemaps env spec-equiv)))
 :rule-classes :congruence)