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

Segment-driverlist-deoverlap

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

Signature

(segment-driverlist-deoverlap lsb x) → new-x

Arguments

lsb — Guard (natp lsb).

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

Returns

new-x — Type (segment-driverlist-p new-x).

We iterate from LSB=0, at each iteration finding the biggest chunk starting at the current LSB such that there are no segment boundaries inside the chunk, then incrementing LSB by that chunk size for the next iteration.

The ordering of the driverlist, sorted by increasing LSB then increasing width, usually allows us to throw out a prefix of the list whenever we incrase the LSB, since any segments that end before the current LSB are no longer relevant.

At each iteration, we first find the chunk width by taking the minimum of all segment endpoints greater than the current LSB, minus the LSB. Then we collect all drivers that overlap with the chunk between LSB and LSB+width-1, sort them by drive strength, and resolve them together to create one driver for that segment. The next LSB is then LSB+width, and we discard any leading elements of the segment list whose segments end before that point.

Definitions and Theorems

Function: segment-driverlist-deoverlap

(defun segment-driverlist-deoverlap (lsb x)
  (declare (xargs :guard (and (natp lsb)
                              (segment-driverlist-p x))))
  (declare (xargs :guard (segment-drivers-ordered-p x)))
  (let ((__function__ 'segment-driverlist-deoverlap))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         (width (segment-driverlist-chunk-width lsb x))
         ((unless width) nil)
         (drivers (segment-driverlist-collect-chunk lsb width x))
         (value (driverlist->svex (drivestrength-sort drivers)))
         (next-lsb (+ width (lnfix lsb)))
         (tail (segment-driverlist-chunk-tail next-lsb x)))
      (cons (make-segment-driver :lsb lsb
                                 :width width
                                 :value value)
            (segment-driverlist-deoverlap next-lsb tail)))))

Theorem: segment-driverlist-p-of-segment-driverlist-deoverlap

(defthm segment-driverlist-p-of-segment-driverlist-deoverlap
  (b* ((new-x (segment-driverlist-deoverlap lsb x)))
    (segment-driverlist-p new-x))
  :rule-classes :rewrite)

Theorem: lsb-car-of-segment-driverlist-deoverlap

(defthm lsb-car-of-segment-driverlist-deoverlap
  (b* ((?new-x (segment-driverlist-deoverlap lsb x)))
    (implies (consp new-x)
             (equal (segment-driver->lsb (car new-x))
                    (nfix lsb)))))

Theorem: segment-drivers-disjoint-p-of-segment-driverlist-deoverlap

(defthm segment-drivers-disjoint-p-of-segment-driverlist-deoverlap
  (b* ((?new-x (segment-driverlist-deoverlap lsb x)))
    (segment-drivers-disjoint-p new-x)))

Theorem: vars-of-segment-driverlist-deoverlap

(defthm vars-of-segment-driverlist-deoverlap
 (b* ((?new-x (segment-driverlist-deoverlap lsb x)))
  (implies (not (member-equal v (segment-driverlist-vars x)))
           (not (member-equal v (segment-driverlist-vars new-x))))))

Theorem: segment-driverlist-deoverlap-of-nfix-lsb

(defthm segment-driverlist-deoverlap-of-nfix-lsb
  (equal (segment-driverlist-deoverlap (nfix lsb)
                                       x)
         (segment-driverlist-deoverlap lsb x)))

Theorem: segment-driverlist-deoverlap-nat-equiv-congruence-on-lsb

(defthm segment-driverlist-deoverlap-nat-equiv-congruence-on-lsb
  (implies (nat-equiv lsb lsb-equiv)
           (equal (segment-driverlist-deoverlap lsb x)
                  (segment-driverlist-deoverlap lsb-equiv x)))
  :rule-classes :congruence)

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

(defthm segment-driverlist-deoverlap-of-segment-driverlist-fix-x
  (equal
       (segment-driverlist-deoverlap lsb (segment-driverlist-fix x))
       (segment-driverlist-deoverlap lsb x)))

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

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