• 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-param-bindings

Generating parametrized g-bindings from an SVTV using gl::flex-bindings.

Signature

(svtv-flex-param-bindings svtv in-alist) → *

Arguments

svtv — Guard (svtv-p svtv).

in-alist — Each element is (list case-spec-alist auto-bindings) or (list case-spec-alist auto-bindings :arrange arrange).

Definitions and Theorems

Function: svtv-flex-param-bindings

(defun
 svtv-flex-param-bindings (svtv in-alist)
 (declare (xargs :guard (svtv-p svtv)))
 (let
   ((__function__ 'svtv-flex-param-bindings))
   (declare (ignorable __function__))
   (b* (((when (atom in-alist)) nil)
        (case1 (car in-alist))
        ((unless (and (true-listp case1)
                      (or (eql (len case1) 2)
                          (and (eql (len case1) 4)
                               (eq (nth 2 case1) :arrange)))))
         (raise "Unsupported entry in svtv-flex-param-bindings: ~x0"
                case1))
        ((list params
               auto-bindings ?arrange-keyword arrange)
         case1))
       (cons (list params
                   (svtv-flex-bindings svtv auto-bindings
                                       :arrange arrange))
             (svtv-flex-param-bindings svtv (cdr in-alist))))))