• 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
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
        • Alias-normalization
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
        • Compile.lisp
        • Assign->segment-drivers
        • Segment-driver-map-resolve
        • Assigns->segment-drivers
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-compilation

Assigns->segment-drivers

For a list of assignments of driving expressions to LHSes, produce an alist mapping each variable from the LHSes to the full list of segment drivers for that variable.

Signature

(assigns->segment-drivers x) → segment-driver-map

Arguments

x — Guard (assigns-p x).

Returns

segment-driver-map — Type (segment-driver-map-p segment-driver-map).

Definitions and Theorems

Function: assigns->segment-drivers

(defun assigns->segment-drivers (x)
  (declare (xargs :guard (assigns-p x)))
  (let ((__function__ 'assigns->segment-drivers))
    (declare (ignorable __function__))
    (fast-alist-free
         (fast-alist-clean (assigns->segment-drivers-aux x nil)))))

Theorem: segment-driver-map-p-of-assigns->segment-drivers

(defthm segment-driver-map-p-of-assigns->segment-drivers
  (b* ((segment-driver-map (assigns->segment-drivers x)))
    (segment-driver-map-p segment-driver-map))
  :rule-classes :rewrite)

Theorem: vars-of-assigns->segment-drivers

(defthm vars-of-assigns->segment-drivers
 (implies
  (not (member v (assigns-vars x)))
  (not
     (member
          v
          (segment-driver-map-vars (assigns->segment-drivers x))))))

Theorem: hons-assoc-equal-of-assigns->segment-drivers

(defthm hons-assoc-equal-of-assigns->segment-drivers
  (implies (not (member v (assigns-vars x)))
           (not (hons-assoc-equal v (assigns->segment-drivers x)))))

Theorem: assigns->segment-drivers-of-assigns-fix-x

(defthm assigns->segment-drivers-of-assigns-fix-x
  (equal (assigns->segment-drivers (assigns-fix x))
         (assigns->segment-drivers x)))

Theorem: assigns->segment-drivers-assigns-equiv-congruence-on-x

(defthm assigns->segment-drivers-assigns-equiv-congruence-on-x
  (implies (assigns-equiv x x-equiv)
           (equal (assigns->segment-drivers x)
                  (assigns->segment-drivers x-equiv)))
  :rule-classes :congruence)