• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
      • Fgl
      • Vwsim
      • 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.