• 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

Assign->segment-drivers

From an assignment to an LHS, accumulate the segment-drivers for each variable mentioned.

Signature

(assign->segment-drivers lhs offset dr acc) → assigns

Arguments

lhs — Guard (lhs-p lhs).

offset — Guard (natp offset).

dr — Guard (driver-p dr).

acc — accumulator.
    Guard (segment-driver-map-p acc).

Returns

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

For example, suppose we have the following Verilog code:

wire [10:0] a;
wire [8:1] b;
wire [3:2] c;
wire [12:0] foo;
assign { a[8:3], b[5:1], c } = foo;

We split this assignment into three separate assignments like this:

assign a[8:3] = foo[12:7];
assign b[5:1] = foo[6:2];
assign c[3:2] = foo[1:0];

Then we accumulate the assignments for a, b, and c onto lists of collected assignments for each one. The representation for each such assignment is a segment-driver which gives the range of the LHS variable that is assigned, the expression to be assigned to it, and the drive strength. These are collected for each LHS variable into a mapping from the LHS variables to their list of segment drivers.

Definitions and Theorems

Function: assign->segment-drivers

(defun assign->segment-drivers (lhs offset dr acc)
  (declare (xargs :guard (and (lhs-p lhs)
                              (natp offset)
                              (driver-p dr)
                              (segment-driver-map-p acc))))
  (let ((__function__ 'assign->segment-drivers))
    (declare (ignorable __function__))
    (b* (((mv first rest) (lhs-decomp lhs))
         (acc (segment-driver-map-fix acc))
         ((unless first) acc)
         ((lhrange first) first)
         (offset (lnfix offset))
         ((when (eq (lhatom-kind first.atom) :z))
          (assign->segment-drivers rest (+ offset first.w)
                                   dr acc))
         ((lhatom-var first.atom))
         ((driver dr))
         (new-driver
              (make-segment-driver :value (svex-rsh offset dr.value)
                                   :strength dr.strength
                                   :lsb first.atom.rsh
                                   :width first.w))
         (rest-drivers (cdr (hons-get first.atom.name acc)))
         (acc (hons-acons first.atom.name
                          (cons new-driver rest-drivers)
                          acc)))
      (assign->segment-drivers rest (+ offset first.w)
                               dr acc))))

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

(defthm segment-driver-map-p-of-assign->segment-drivers
  (b* ((assigns (assign->segment-drivers lhs offset dr acc)))
    (segment-driver-map-p assigns))
  :rule-classes :rewrite)

Theorem: assign->segment-drivers-of-lhs-fix-lhs

(defthm assign->segment-drivers-of-lhs-fix-lhs
  (equal (assign->segment-drivers (lhs-fix lhs)
                                  offset dr acc)
         (assign->segment-drivers lhs offset dr acc)))

Theorem: assign->segment-drivers-lhs-equiv-congruence-on-lhs

(defthm assign->segment-drivers-lhs-equiv-congruence-on-lhs
 (implies (lhs-equiv lhs lhs-equiv)
          (equal (assign->segment-drivers lhs offset dr acc)
                 (assign->segment-drivers lhs-equiv offset dr acc)))
 :rule-classes :congruence)

Theorem: assign->segment-drivers-of-nfix-offset

(defthm assign->segment-drivers-of-nfix-offset
  (equal (assign->segment-drivers lhs (nfix offset)
                                  dr acc)
         (assign->segment-drivers lhs offset dr acc)))

Theorem: assign->segment-drivers-nat-equiv-congruence-on-offset

(defthm assign->segment-drivers-nat-equiv-congruence-on-offset
 (implies (nat-equiv offset offset-equiv)
          (equal (assign->segment-drivers lhs offset dr acc)
                 (assign->segment-drivers lhs offset-equiv dr acc)))
 :rule-classes :congruence)

Theorem: assign->segment-drivers-of-driver-fix-dr

(defthm assign->segment-drivers-of-driver-fix-dr
  (equal (assign->segment-drivers lhs offset (driver-fix dr)
                                  acc)
         (assign->segment-drivers lhs offset dr acc)))

Theorem: assign->segment-drivers-driver-equiv-congruence-on-dr

(defthm assign->segment-drivers-driver-equiv-congruence-on-dr
 (implies (driver-equiv dr dr-equiv)
          (equal (assign->segment-drivers lhs offset dr acc)
                 (assign->segment-drivers lhs offset dr-equiv acc)))
 :rule-classes :congruence)

Theorem: assign->segment-drivers-of-segment-driver-map-fix-acc

(defthm assign->segment-drivers-of-segment-driver-map-fix-acc
 (equal
    (assign->segment-drivers lhs
                             offset dr (segment-driver-map-fix acc))
    (assign->segment-drivers lhs offset dr acc)))

Theorem: assign->segment-drivers-segment-driver-map-equiv-congruence-on-acc

(defthm
 assign->segment-drivers-segment-driver-map-equiv-congruence-on-acc
 (implies (segment-driver-map-equiv acc acc-equiv)
          (equal (assign->segment-drivers lhs offset dr acc)
                 (assign->segment-drivers lhs offset dr acc-equiv)))
 :rule-classes :congruence)

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

(defthm vars-of-assign->segment-drivers
 (implies
  (and (not (member v (lhs-vars lhs)))
       (not (member v (svex-vars (driver->value dr))))
       (not (member v (segment-driver-map-vars acc))))
  (not (member v
               (segment-driver-map-vars
                    (assign->segment-drivers lhs offset dr acc))))))

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

(defthm hons-assoc-equal-of-assign->segment-drivers
 (implies
  (and (not (member v (lhs-vars lhs)))
       (not (hons-assoc-equal v (segment-driver-map-fix acc))))
  (not
   (hons-assoc-equal v
                     (assign->segment-drivers lhs offset dr acc)))))