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

Generating G-bindings from an SVTV in a particular way.

Signature

(svtv-easy-bindings svtv order) → *

Arguments

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

order — The variable order you want to use.

(svtv-easy-bindings svtv order) is a macro for proving theorems about symbolic-test-vectors using gl. It returns a list of G-bindings for use with ACL2::def-gl-thm. That is, you can write something like:

(def-gl-thm foo
   ...
   :g-bindings
   (svtv-easy-bindings (my-svtv) '(opcode size special (:mix a b) c)))

This is probably only useful when:

• You are using GL in BDD mode, not some AIG or SAT based mode.
• You are running into performance problems when using the default -autobinds from the defsvtv.
• You want to see if a different variable order performs better.

To use svtv-easy-bindings, you just list (a subset of) the SVTV inputs in priority order. For instance, in the above example, the opcode will get the smallest indices, then size next, etc. You do not have to list all of the SVTV variables. Any unmentioned variables will be assigned indices after mentioned variables.

As in gl::auto-bindings, you can also use (:mix a b c ...) to interleave the bits of a, b, c, ...; note that for this to work these variables must all share the same width. This is generally useful for data buses that are going to be combined together.

An especially nice feature of easy-bindings is that they automatically adjust when inputs to the SVTV are resized, when new inputs are added, and when irrelevant inputs are removed.

Definitions and Theorems

Function: svtv-easy-bindings

(defun
 svtv-easy-bindings (svtv order)
 (declare (xargs :guard (svtv-p svtv)))
 (let
  ((__function__ 'svtv-easy-bindings))
  (declare (ignorable __function__))
  (b*
   ((binds (svtv-easy-bindings-main order svtv))
    (unbound
       (set-difference-equal (svtv->ins svtv)
                             (svtv-easy-bindings-svtv-vars order))))
   (gl::auto-bindings-fn
        (append binds
                (svtv-easy-bindings-main unbound svtv))))))