• 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
          • 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
  • Def-svtv-ideal

Svtv-idealize-internals

Umbrella topic for internal concepts used in the proofs for the svtv-idealize framework.

Subtopics

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.