• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
      • Svex-compilation
        • Alias-normalization
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
        • Compile.lisp
        • Assign->netassigns
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svex-compilation

Assign->netassigns

Turns an assignment (possibly to parts of wires) into several assignments to whole wires.

Signature

(assign->netassigns lhs offset dr acc) → assigns

Arguments

lhs — Guard (lhs-p lhs).

offset — Guard (natp offset).

dr — Guard (driver-p dr).

acc — accumulator.
    Guard (netassigns-p acc).

Returns

assigns — Type (netassigns-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 would turn this assignment into three separate assignments, essentially like this:

assign a = { 2'bz, foo[12:7], 3'bz };
assign b = { 3'bz, foo[6:2] };
assign c = foo[1:0];

The representation in SVEX is a bit different than the Verilog notation suggests: we don't know each variable's width and we don't have a part-select operator -- instead, on the left-hand side, we have an lhs structure forming the concatenation, and on the right-hand side use shifts concatenations to emulate part-selecting from the RHS expression. So a more accurate view would be as follows, where a[3+:6] is meant to represent an lhatom of width 6 and right-shift 3; inf is used to signify an infinite-width constant; and { ... , 2'foo } signifies concatenating the ... with 2 bits of foo:

assign { a[3+:6], b[1+:5], c[2+:2] } = foo;

becomes

assign c = { 'z, 2'foo };
assign b = { 'z, 5'(foo >> 2) };
assign a = { 'z, 6'(foo >> 7), 3'bz };

Definitions and Theorems

Function: assign->netassigns

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

Theorem: netassigns-p-of-assign->netassigns

(defthm netassigns-p-of-assign->netassigns
        (b* ((assigns (assign->netassigns lhs offset dr acc)))
            (netassigns-p assigns))
        :rule-classes :rewrite)

Theorem: assign->netassigns-of-lhs-fix-lhs

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

Theorem: assign->netassigns-lhs-equiv-congruence-on-lhs

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

Theorem: assign->netassigns-of-nfix-offset

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

Theorem: assign->netassigns-nat-equiv-congruence-on-offset

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

Theorem: assign->netassigns-of-driver-fix-dr

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

Theorem: assign->netassigns-driver-equiv-congruence-on-dr

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

Theorem: assign->netassigns-of-netassigns-fix-acc

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

Theorem: assign->netassigns-netassigns-equiv-congruence-on-acc

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

Theorem: vars-of-assign->netassigns

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

Theorem: hons-assoc-equal-of-assign->netassigns

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