• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
      • Svex-compilation
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
        • Svtv-easy-bindings
        • Svtv-flex-param-bindings
        • Svtv-flex-bindings
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Symbolic-test-vector

Svtv-flex-bindings

Generating G-bindings from an SVTV using gl::flex-bindings.

Signature

(svtv-flex-bindings svtv order &key arrange) → *

Arguments

svtv — The SVTV you are dealing with.
    Guard (svtv-p svtv).

order — The variable order you want to use.

arrange — Arrangement of the indices.

Definitions and Theorems

Function: svtv-flex-bindings-fn

(defun
 svtv-flex-bindings-fn
 (svtv order arrange)
 (declare (xargs :guard (svtv-p svtv)))
 (let
  ((__function__ 'svtv-flex-bindings))
  (declare (ignorable __function__))
  (b*
    ((binds (svtv-easy-bindings-main order svtv))
     (arrange1 (or arrange
                   (gl::auto-bindings-list-collect-arrange
                        (gl::auto-bind-xlate-list binds nil))))
     (unbound
          (set-difference-equal (svtv->ins svtv)
                                (strip-cars (strip-cdrs arrange1))))
     (unbound-binds (svtv-easy-bindings-main unbound svtv))
     (unbound-arrange
          (gl::auto-bindings-list-collect-arrange
               (gl::auto-bind-xlate-list unbound-binds nil))))
    (gl::flex-bindings-fn (append binds unbound-binds)
                          (append arrange1 unbound-arrange)
                          0))))