		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-moddb.lisp

Vl-streaming-unpack-to-svex-assign-top

Resolve an assignment where the LHS is a streaming concatenation, after converting the RHS expression to svex (untyped).

Signature
(vl-streaming-unpack-to-svex-assign-top lhs rhs orig-x rhs-size ss scopes) → (mv vttree assigns)
Arguments: lhs — Guard (vl-expr-p lhs).; rhs — Guard (sv::svex-p rhs).; orig-x — Guard (vl-assign-p orig-x).; rhs-size — remaining number of least-significant bits in the RHS that haven't been used yet.
Guard (natp rhs-size).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).
Returns: vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .; assigns — Type (implies (sv::svarlist-addr-p (sv::svex-vars rhs)) (and (sv::assigns-p assigns) (sv::svarlist-addr-p (sv::assigns-vars assigns)))) .

To see how simulators treat streaming concatenations on the LHS, it is most instructive to look at some examples.

First, consider the example in "sv/cosims/stream3/test.sv":

logic [3:0] in;
logic [3:0] out;
assign {<< 3 {out}} = in;

When {<< 3 {a}} occurs on the RHS of an assignment (and a is 4 bits wide), it basically means the same thing as { a[2:0], a[3] }. So we might think that we'd get the same results for guess1 if we assign it as:

logic [3:0] guess1;
assign { guess1[2:0], guess1[3] } = in;

But this isn't the case, at least in the major commercial simulators, VCS and NCVerilog. Instead, when we run it on the following inputs:

we get the following outputs:

out: 0010, guess1: 1000
out: 0100, guess1: 0001
out: 1000, guess1: 0010
out: 0001, guess1: 0100

Actually, what this corresponds to is:

assign out = { in[2:0], in[3] };

or:

assign out = {<< 3 {in}};

This doesn't make a lot of sense, but the pattern holds generally: if you see a streaming concatenation on the LHS, it means the same as if you put it on the RHS. (A complication in testing this rule is that the LHS and RHS need to be the same size for both to be allowed.)

This rule is complicated by the fact that streaming concatenations can be nested, and can have more than one expression concatenated together. It is also not clear how to treat cases where the RHS has more bits than the LHS. We reverse engineered the behavior of VCS using the example in "sv/cosims/stream4/test.sv". (NCVerilog doesn't fully support multiple streaming expressions inside a concatenation on the LHS.)

logic [31:0] in;
logic [8:0] out1;
logic [6:0] out2;
assign {<< 5 {{<< 3 {out1}}, out2}} = in[31:0];

When run on the input pattern

00000000000000000000000000000001
00000000000000000000000000000010
00000000000000000000000000000100
...

this produces the results:

out1 000010000, out2 0000000
out1 000100000, out2 0000000
out1 000000001, out2 0000000
out1 000000010, out2 0000000
out1 000000100, out2 0000000
out1 000000000, out2 1000000
out1 001000000, out2 0000000
out1 010000000, out2 0000000
out1 100000000, out2 0000000
out1 000001000, out2 0000000
out1 000000000, out2 0000010
out1 000000000, out2 0000100
out1 000000000, out2 0001000
out1 000000000, out2 0010000
out1 000000000, out2 0100000
out1 000000000, out2 0000000
out1 000000000, out2 0000000
out1 000000000, out2 0000000
out1 000000000, out2 0000000
out1 000000000, out2 0000001

This turns out to be equivalent to the following:

logic [31:0] temp1;
logic [15:0] temp2;
logic [8:0] temp3;
logic [6:0] temp4;
assign temp1 = {<< 5 {in[31:0]}};
assign temp2 = temp1 >> 16;
assign {temp3, temp4} = temp2;
assign out2 = temp4;
assign out1 = {<< 3 {temp3}};

It's not clear why we should think this is the correct behavior, but we at least can derive an algorithm from it:

Move the outermost streaming concatenation operator to the RHS (obtaining temp1, in the example).
Compute the bit widths of LHS and RHS and right-shift the RHS by rhswidth - lhswidth (obtaining temp2, in this example).
Chop up the RHS into chunks matching the sizes of the concatenated subexpressions of the LHS (obtaining temp3, temp4).
Make a new assignment of each chunk to its corresponding LHS subexpression, and for each assignment created that has a LHS streaming concatenation, repeat this process. (Thus we assign out2 to temp4 and end up assigning out1 to {<< 3 {temp3}}).

Note that when repeating the process for the last step, we can skip step 2, because the sizes match by construction.

Definitions and Theorems

Function: vl-streaming-unpack-to-svex-assign-top

(defun vl-streaming-unpack-to-svex-assign-top
       (lhs rhs orig-x rhs-size ss scopes)
 (declare (xargs :guard (and (vl-expr-p lhs)
                             (sv::svex-p rhs)
                             (vl-assign-p orig-x)
                             (natp rhs-size)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (declare (xargs :guard (vl-expr-case lhs :vl-stream)))
 (let ((__function__ 'vl-streaming-unpack-to-svex-assign-top))
  (declare (ignorable __function__))
  (b*
   (((vl-stream lhs) (vl-expr-fix lhs))
    (rhs-size (lnfix rhs-size))
    (orig-x (vl-assign-fix orig-x))
    (vttree nil)
    ((vmv vttree ?lhs-svex ?lhs-type lhs-size)
     (vl-expr-to-svex-untyped lhs ss scopes))
    ((unless lhs-size)
     (mv
       (vfatal :type :vl-bad-stream-assignment
               :msg "~a0: couldn't size LHS streaming concatenation"
               :args (list orig-x))
       nil))
    ((mv err slicesize)
     (if (eq lhs.dir :left)
         (vl-slicesize-resolve lhs.size ss scopes)
       (mv nil 1)))
    ((when err)
     (mv
      (vfatal
       :type :vl-expr-to-svex-fail
       :msg
       "Failed to resolve slice size of streaming ~
                               concat expression ~a0: ~@1"
       :args (list lhs err))
      nil))
    ((mv vttree rhs rhs-size)
     (cond
      ((< rhs-size lhs-size)
       (mv
        (vfatal
         :type :vl-bad-stream-assignment
         :msg
         "~a0: SystemVerilog prohibits streaming assignments
                                   where a streaming concatenation expression (either
                                   LHS or RHS) is larger than the other."
         :args (list orig-x))
        (sv::svcall sv::concat
                    (svex-int (- lhs-size rhs-size))
                    (svex-int 0)
                    rhs)
        lhs-size))
      (t (mv vttree rhs rhs-size))))
    (rhs-bitstream (if (eq lhs.dir :left)
                       (sv::svcall sv::blkrev (svex-int rhs-size)
                                   (svex-int slicesize)
                                   rhs)
                     rhs))
    (rhs-shift
         (if (< lhs-size rhs-size)
             (sv::svcall sv::rsh (svex-int (- rhs-size lhs-size))
                         rhs-bitstream)
           rhs-bitstream))
    ((vmv vttree assigns)
     (vl-streamexprlist-unpack-to-svex-assign
          lhs.parts
          rhs-shift lhs-size ss scopes)))
   (mv vttree assigns))))

Theorem: return-type-of-vl-streaming-unpack-to-svex-assign-top.vttree

(defthm return-type-of-vl-streaming-unpack-to-svex-assign-top.vttree
 (b* (((mv ?vttree ?assigns)
       (vl-streaming-unpack-to-svex-assign-top
            lhs rhs orig-x rhs-size ss scopes)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-streaming-unpack-to-svex-assign-top.assigns

(defthm
      return-type-of-vl-streaming-unpack-to-svex-assign-top.assigns
 (b* (((mv ?vttree ?assigns)
       (vl-streaming-unpack-to-svex-assign-top
            lhs rhs orig-x rhs-size ss scopes)))
   (implies (sv::svarlist-addr-p (sv::svex-vars rhs))
            (and (sv::assigns-p assigns)
                 (sv::svarlist-addr-p (sv::assigns-vars assigns)))))
 :rule-classes :rewrite)

Theorem: vl-streaming-unpack-to-svex-assign-top-of-vl-expr-fix-lhs

(defthm vl-streaming-unpack-to-svex-assign-top-of-vl-expr-fix-lhs
  (equal (vl-streaming-unpack-to-svex-assign-top
              (vl-expr-fix lhs)
              rhs orig-x rhs-size ss scopes)
         (vl-streaming-unpack-to-svex-assign-top
              lhs rhs orig-x rhs-size ss scopes)))

Theorem: vl-streaming-unpack-to-svex-assign-top-vl-expr-equiv-congruence-on-lhs

(defthm
 vl-streaming-unpack-to-svex-assign-top-vl-expr-equiv-congruence-on-lhs
 (implies (vl-expr-equiv lhs lhs-equiv)
          (equal (vl-streaming-unpack-to-svex-assign-top
                      lhs rhs orig-x rhs-size ss scopes)
                 (vl-streaming-unpack-to-svex-assign-top
                      lhs-equiv
                      rhs orig-x rhs-size ss scopes)))
 :rule-classes :congruence)

Theorem: vl-streaming-unpack-to-svex-assign-top-of-svex-fix-rhs

(defthm vl-streaming-unpack-to-svex-assign-top-of-svex-fix-rhs
 (equal
  (vl-streaming-unpack-to-svex-assign-top lhs (sv::svex-fix rhs)
                                          orig-x rhs-size ss scopes)
  (vl-streaming-unpack-to-svex-assign-top
       lhs rhs orig-x rhs-size ss scopes)))

Theorem: vl-streaming-unpack-to-svex-assign-top-svex-equiv-congruence-on-rhs

(defthm
 vl-streaming-unpack-to-svex-assign-top-svex-equiv-congruence-on-rhs
 (implies (sv::svex-equiv rhs rhs-equiv)
          (equal (vl-streaming-unpack-to-svex-assign-top
                      lhs rhs orig-x rhs-size ss scopes)
                 (vl-streaming-unpack-to-svex-assign-top
                      lhs
                      rhs-equiv orig-x rhs-size ss scopes)))
 :rule-classes :congruence)

Theorem: vl-streaming-unpack-to-svex-assign-top-of-vl-assign-fix-orig-x

(defthm
     vl-streaming-unpack-to-svex-assign-top-of-vl-assign-fix-orig-x
  (equal (vl-streaming-unpack-to-svex-assign-top
              lhs rhs (vl-assign-fix orig-x)
              rhs-size ss scopes)
         (vl-streaming-unpack-to-svex-assign-top
              lhs rhs orig-x rhs-size ss scopes)))

Theorem: vl-streaming-unpack-to-svex-assign-top-vl-assign-equiv-congruence-on-orig-x

(defthm
 vl-streaming-unpack-to-svex-assign-top-vl-assign-equiv-congruence-on-orig-x
 (implies (vl-assign-equiv orig-x orig-x-equiv)
          (equal (vl-streaming-unpack-to-svex-assign-top
                      lhs rhs orig-x rhs-size ss scopes)
                 (vl-streaming-unpack-to-svex-assign-top
                      lhs
                      rhs orig-x-equiv rhs-size ss scopes)))
 :rule-classes :congruence)

Theorem: vl-streaming-unpack-to-svex-assign-top-of-nfix-rhs-size

(defthm vl-streaming-unpack-to-svex-assign-top-of-nfix-rhs-size
  (equal (vl-streaming-unpack-to-svex-assign-top
              lhs rhs orig-x (nfix rhs-size)
              ss scopes)
         (vl-streaming-unpack-to-svex-assign-top
              lhs rhs orig-x rhs-size ss scopes)))

Theorem: vl-streaming-unpack-to-svex-assign-top-nat-equiv-congruence-on-rhs-size

(defthm
 vl-streaming-unpack-to-svex-assign-top-nat-equiv-congruence-on-rhs-size
 (implies (acl2::nat-equiv rhs-size rhs-size-equiv)
          (equal (vl-streaming-unpack-to-svex-assign-top
                      lhs rhs orig-x rhs-size ss scopes)
                 (vl-streaming-unpack-to-svex-assign-top
                      lhs
                      rhs orig-x rhs-size-equiv ss scopes)))
 :rule-classes :congruence)

Theorem: vl-streaming-unpack-to-svex-assign-top-of-vl-scopestack-fix-ss

(defthm
     vl-streaming-unpack-to-svex-assign-top-of-vl-scopestack-fix-ss
  (equal (vl-streaming-unpack-to-svex-assign-top
              lhs rhs
              orig-x rhs-size (vl-scopestack-fix ss)
              scopes)
         (vl-streaming-unpack-to-svex-assign-top
              lhs rhs orig-x rhs-size ss scopes)))

Theorem: vl-streaming-unpack-to-svex-assign-top-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-streaming-unpack-to-svex-assign-top-vl-scopestack-equiv-congruence-on-ss
 (implies (vl-scopestack-equiv ss ss-equiv)
          (equal (vl-streaming-unpack-to-svex-assign-top
                      lhs rhs orig-x rhs-size ss scopes)
                 (vl-streaming-unpack-to-svex-assign-top
                      lhs
                      rhs orig-x rhs-size ss-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-streaming-unpack-to-svex-assign-top-of-vl-elabscopes-fix-scopes

(defthm
 vl-streaming-unpack-to-svex-assign-top-of-vl-elabscopes-fix-scopes
 (equal (vl-streaming-unpack-to-svex-assign-top
             lhs rhs orig-x
             rhs-size ss (vl-elabscopes-fix scopes))
        (vl-streaming-unpack-to-svex-assign-top
             lhs rhs orig-x rhs-size ss scopes)))

Theorem: vl-streaming-unpack-to-svex-assign-top-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-streaming-unpack-to-svex-assign-top-vl-elabscopes-equiv-congruence-on-scopes
 (implies (vl-elabscopes-equiv scopes scopes-equiv)
          (equal (vl-streaming-unpack-to-svex-assign-top
                      lhs rhs orig-x rhs-size ss scopes)
                 (vl-streaming-unpack-to-svex-assign-top
                      lhs
                      rhs orig-x rhs-size ss scopes-equiv)))
 :rule-classes :congruence)