		Search-engine friendly clone of the ACL2 documentation.

Argument-partitioning

Vl-partition-msb-bitslices

Group up a list of bits into N-bit concatenations.

Signature
(vl-partition-msb-bitslices n x) → new-exprs
Arguments: n — A positive number that must evenly divide (len x).
Guard (posp n).; x — A list of 1-bit unsigned expressions.
Guard (vl-exprlist-p x).
Returns: new-exprs — Concatenations of n successive bits of x.
Type (vl-exprlist-p new-exprs).

The basic way that we partition an expression into N-bit slices is to break it up into individual bits with vl-msb-bitslice-expr, then group these bits together into N-bit concatenations. Typically we expect that x is the result of calling vl-msb-bitslice-expr to slice up an expression into such bits.

We return a new list of expressions, each of is a concatenation of n successive bits of x. For instance, if

x is (bit_99 bit_98 ... bit_0), and
n is 5,

Then the resulting list of expressions will be:

{bit_99, bit_98, bit_97, bit_96, bit_95}
{bit_94, bit_93, bit_92, bit_91, bit_90}
...
{bit_4, bit_3, bit_2, bit_1, bit_0}

We prove that the resulting expressions all have width n, that there are the right number of resulting expressions, and that they are all well-typed assuming that the input bit-expressions are well-typed.

Aesthetic Notes

An arguably unfortunate consequence of our partitioning approach is that the resulting concatenations of bits can be large and ugly in certain cases. For instance, part selects like foo[31:0] will get blown up into things like { foo[31], foo[30], ..., foo[0] }, which is overly verbose and perhaps hard to read.

My original implementation of partitioning also had a "cleaning" phase that tried to correct for this, essentially by identifying these descending sequences of bit-selects and re-assembling them into part-selects. But I no longer to implement such a cleaning phase. My rationale is that:

Aesthetics here are not very important because instance arrays are not that common in the first place, so we are not going to be breaking up very many expressions in this potentially bad way, and
Not cleaning avoids any potential errors in the cleaning code. This is not much of an argument since the cleaning code is relatively simple, but it still has some merit.

NOTE: we now have expr-cleaning code that can do this cleaning. We don't currently use it here, in case it has any bugs, but perhaps we should re-integrate it.

Definitions and Theorems

Function: vl-partition-msb-bitslices

(defun vl-partition-msb-bitslices (n x)
 (declare (xargs :guard (and (posp n) (vl-exprlist-p x))))
 (declare
   (xargs :guard (and (eql (mod (len x) n) 0)
                      (all-equalp 1 (vl-exprlist->finalwidths x)))))
 (let ((__function__ 'vl-partition-msb-bitslices))
   (declare (ignorable __function__))
   (b* ((n (lposfix n))
        ((when (eql n 0)) nil)
        ((when (< (len x) n)) nil))
     (cons (make-vl-nonatom :op :vl-concat
                            :args (first-n n x)
                            :finalwidth n
                            :finaltype :vl-unsigned
                            :atts nil)
           (vl-partition-msb-bitslices n (rest-n n x))))))

Theorem: vl-exprlist-p-of-vl-partition-msb-bitslices

(defthm vl-exprlist-p-of-vl-partition-msb-bitslices
  (b* ((new-exprs (vl-partition-msb-bitslices n x)))
    (vl-exprlist-p new-exprs))
  :rule-classes :rewrite)

Theorem: len-of-vl-partition-msb-bitslices

(defthm len-of-vl-partition-msb-bitslices
  (equal (len (vl-partition-msb-bitslices n x))
         (floor (len x) (pos-fix n))))

Theorem: vl-exprlist->finalwidths-of-vl-partition-msb-bitslices

(defthm vl-exprlist->finalwidths-of-vl-partition-msb-bitslices
  (equal (vl-exprlist->finalwidths (vl-partition-msb-bitslices n x))
         (replicate (floor (len x) (pos-fix n))
                    (pos-fix n))))

Theorem: vl-exprlist->finaltypes-of-vl-partition-msb-bitslices

(defthm vl-exprlist->finaltypes-of-vl-partition-msb-bitslices
  (equal (vl-exprlist->finaltypes (vl-partition-msb-bitslices n x))
         (replicate (floor (len x) (pos-fix n))
                    :vl-unsigned)))

Theorem: vl-exprlist-welltyped-p-of-vl-partition-msb-bitslices

(defthm vl-exprlist-welltyped-p-of-vl-partition-msb-bitslices
  (implies
       (and (force (vl-exprlist-welltyped-p x))
            (force (all-equalp 1 (vl-exprlist->finalwidths x))))
       (vl-exprlist-welltyped-p (vl-partition-msb-bitslices n x))))

Theorem: vl-partition-msb-bitslices-of-pos-fix-n

(defthm vl-partition-msb-bitslices-of-pos-fix-n
  (equal (vl-partition-msb-bitslices (pos-fix n)
                                     x)
         (vl-partition-msb-bitslices n x)))

Theorem: vl-partition-msb-bitslices-pos-equiv-congruence-on-n

(defthm vl-partition-msb-bitslices-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-partition-msb-bitslices n x)
                  (vl-partition-msb-bitslices n-equiv x)))
  :rule-classes :congruence)

Theorem: vl-partition-msb-bitslices-of-vl-exprlist-fix-x

(defthm vl-partition-msb-bitslices-of-vl-exprlist-fix-x
  (equal (vl-partition-msb-bitslices n (vl-exprlist-fix x))
         (vl-partition-msb-bitslices n x)))

Theorem: vl-partition-msb-bitslices-vl-exprlist-equiv-congruence-on-x

(defthm vl-partition-msb-bitslices-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-partition-msb-bitslices n x)
                  (vl-partition-msb-bitslices n x-equiv)))
  :rule-classes :congruence)