Resolve an assignment where the LHS is a streaming concatenation, after converting the RHS expression to svex (untyped).
(vl-streaming-unpack-to-svex-assign-top lhs rhs orig-x rhs-size ss scopes) → (mv vttree 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
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:
0001 0010 0100 1000
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:
Note that when repeating the process for the last step, we can skip step 2, because the sizes match by construction.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)