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

• Segment-driver-map-resolve

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.

Signature

(segment-driverlist-resolve x) → value

Arguments

x — Guard (segment-driverlist-p x).

Returns

value — Type (svex-p value).

This works in three main steps: sort the drivers by LSB and width, resolve each overlap of multiple drivers into a combined driver so that all drivers are nonoverlapping, and finally concatenate the value expressions of this nonoverlapping list of drivers into a single expression.

The complicated part is resolving overlapping drivers; see segment-driverlist-deoverlap.

Definitions and Theorems

Function: segment-driverlist-resolve

(defun segment-driverlist-resolve (x)
  (declare (xargs :guard (segment-driverlist-p x)))
  (let ((__function__ 'segment-driverlist-resolve))
    (declare (ignorable __function__))
    (b* ((sort (segment-drivers-sort (segment-driverlist-fix x)))
         (deoverlap (segment-driverlist-deoverlap 0 sort)))
      (disjoint-segment-drivers->svex deoverlap))))

Theorem: svex-p-of-segment-driverlist-resolve

(defthm svex-p-of-segment-driverlist-resolve
  (b* ((value (segment-driverlist-resolve x)))
    (svex-p value))
  :rule-classes :rewrite)

Theorem: vars-of-segment-drivers-insert

(defthm vars-of-segment-drivers-insert
 (implies
  (and (not (member-equal v (segment-driver-vars elt)))
       (not (member-equal v (segment-driverlist-vars x))))
  (not
   (member-equal
        v
        (segment-driverlist-vars (segment-drivers-insert elt x))))))

Theorem: vars-of-segment-drivers-insertsort

(defthm vars-of-segment-drivers-insertsort
 (implies
  (and (not (member-equal v (segment-driverlist-vars x))))
  (not
   (member-equal
        v
        (segment-driverlist-vars (segment-drivers-insertsort x))))))

Theorem: vars-of-segment-driverlist-resolve

(defthm vars-of-segment-driverlist-resolve
  (b* ((acl2::?value (segment-driverlist-resolve x)))
    (implies (not (member-equal v (segment-driverlist-vars x)))
             (not (member-equal v (svex-vars value))))))

Theorem: segment-driverlist-resolve-of-segment-driverlist-fix-x

(defthm segment-driverlist-resolve-of-segment-driverlist-fix-x
  (equal (segment-driverlist-resolve (segment-driverlist-fix x))
         (segment-driverlist-resolve x)))

Theorem: segment-driverlist-resolve-segment-driverlist-equiv-congruence-on-x

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

Subtopics

Segment-driverlist-deoverlap

Resolve overlapping elements of an ordered list of segment driver objects, resulting in an ordered, nonoverlapping list.