• 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
          • Segment-driverlist-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

Segment-driver-map-resolve

Given an alist mapping each driven variable to its list of segment drivers, resolve this to an svex-alist mapping each variable to its full assignment.

Signature

(segment-driver-map-resolve x) → assigns

Arguments

x — Guard (segment-driver-map-p x).

Returns

assigns — Type (svex-alist-p assigns).

This applies segment-driverlist-resolve to the list of drivers for each variable.

Definitions and Theorems

Function: segment-driver-map-resolve

(defun segment-driver-map-resolve (x)
  (declare (xargs :guard (segment-driver-map-p x)))
  (let ((__function__ 'segment-driver-map-resolve))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((when (atom x)) nil)
              ((unless (mbt (and (consp (car x))
                                 (svar-p (caar x)))))
               (segment-driver-map-resolve (cdr x)))
              ((cons name drivers) (car x))
              (value (segment-driverlist-resolve drivers)))
           (cons (cons name value)
                 (segment-driver-map-resolve (cdr x))))
         :exec
         (if (atom x)
             nil
           (acl2::with-local-nrev
                (segment-driver-map-resolve-nrev x acl2::nrev))))))

Theorem: svex-alist-p-of-segment-driver-map-resolve

(defthm svex-alist-p-of-segment-driver-map-resolve
  (b* ((assigns (segment-driver-map-resolve x)))
    (svex-alist-p assigns))
  :rule-classes :rewrite)

Theorem: vars-of-segment-driver-map-resolve

(defthm vars-of-segment-driver-map-resolve
 (implies
  (not (member v (segment-driver-map-vars x)))
  (and
   (not (member v
                (svex-alist-keys (segment-driver-map-resolve x))))
   (not
       (member v
               (svex-alist-vars (segment-driver-map-resolve x)))))))

Theorem: svex-lookup-under-iff-of-segment-driver-map-resolve

(defthm svex-lookup-under-iff-of-segment-driver-map-resolve
  (b* ((?assigns (segment-driver-map-resolve x)))
    (iff (svex-lookup v assigns)
         (hons-assoc-equal (svar-fix v)
                           (segment-driver-map-fix x)))))

Theorem: segment-driver-map-resolve-of-segment-driver-map-fix-x

(defthm segment-driver-map-resolve-of-segment-driver-map-fix-x
  (equal (segment-driver-map-resolve (segment-driver-map-fix x))
         (segment-driver-map-resolve x)))

Theorem: segment-driver-map-resolve-segment-driver-map-equiv-congruence-on-x

(defthm
 segment-driver-map-resolve-segment-driver-map-equiv-congruence-on-x
 (implies (segment-driver-map-equiv x x-equiv)
          (equal (segment-driver-map-resolve x)
                 (segment-driver-map-resolve x-equiv)))
 :rule-classes :congruence)

Subtopics

Segment-driverlist-resolve

Given the list of drivers for various segments of a variable, turn them into a single svex comprising that variable's full assignment.