Oprewrite
Rewrite expressions to eliminate various operators.
We transform expressions by applying the following rewrite rules.
Note that we do not expect any widths to have been computed at the time this
operation is performed, and so we do not try to preserve any widths.
For our translation to be correct, each of these rules needs to be sound.
That is, choose any Verilog bit vectors for a, b, and c. Then, it needs to be
the case that each left-hand side, above, evaluates to the same thing as its
corresponding right-hand side.
After reading the Verilog spec, we think this is true. In addition, we have
constructed a Verilog test harness (see xf-oprewrite.v) which checks that this
is the case for all Verilog bit vectors of length 4 (i.e., vectors whose bits
are 0, 1, x, or z), and we have established that there are no 4-bit violations
on Cadence.
Operator Elimination Rules
The following rules are useful in that the operators on the left are
completely erased from the parse tree. Hence, we do not need to consider
how to synthesize them or handle them at all!
- +a --> a + 1'sb0
- -a --> 1'sb0 - a
- a && b --> (|a) & (|b)
- a || b --> (|a) | (|b)
- !a --> {~(|a)}
- ~& (a) --> {~( &a )}
- ~| (a) --> {~( |a )}
- ~^ (a) --> {~( ^a )}
- a < b --> {~(a >= b)}
- a > b --> {~(b >= a)}
- a <= b --> b >= a
- a == b --> &(a ~^ b)
- a != b --> |(a ^ b)
- a !== b --> {~(a === b)}
Additional Rules
We also have a couple of rules that help to standardize conditional
expressions. In particular, the first rule here ensures that when we go to
synthesize a conditional operation, we can assume that the "test" argument
has a width of 1. The second rule ensures that if we encounter a (BOZO
is that the right name for this kind of thing?) then then Z is always in the
false branch.
- a ? b : c --> (|a) ? b : c
- a ? z : c --> ~(|a) ? c : z
We also consolidate multiple-concatenations of constint and weirdint values
into a single values. This is important for properly recognizing zatoms in
occform, since designers sometimes write things like
assign foo = a ? b : width{ 1'bz }
Here, if we don't consolidate width{1'bz}, we're not going to recognize
it as a zatom and occform it correctly.
Subtopics
- Vl-op-oprewrite
- Main operator rewriting function.
- Vl-modulelist-oprewrite
- (vl-modulelist-oprewrite x) maps vl-module-oprewrite across a list.
- Vl-expr-oprewrite
- (vl-expr-oprewrite x warnings) rewrites operators throughout the vl-expr-p x and returns (mv warnings-prime x-prime).
- Vl-maybe-delayoreventcontrol-oprewrite
- Rewrite operators throughout a vl-maybe-delayoreventcontrol-p
- Vl-repeateventcontrol-oprewrite
- Rewrite operators throughout a vl-repeateventcontrol-p
- Vl-plainarglist-oprewrite
- Rewrite operators throughout a vl-plainarglist-p
- Vl-namedarglist-oprewrite
- Rewrite operators throughout a vl-namedarglist-p
- Vl-gateinstlist-oprewrite
- Rewrite operators throughout a vl-gateinstlist-p
- Vl-delayoreventcontrol-oprewrite
- Rewrite operators throughout a vl-delayoreventcontrol-p
- Vl-modinstlist-oprewrite
- Rewrite operators throughout a vl-modinstlist-p
- Vl-initiallist-oprewrite
- Rewrite operators throughout a vl-initiallist-p
- Vl-replicate-constint-value
- Generate n copies of a constant integer.
- Vl-evatomlist-oprewrite
- Rewrite operators throughout a vl-evatomlist-p
- Vl-assignlist-oprewrite
- Rewrite operators throughout a vl-assignlist-p
- Vl-arguments-oprewrite
- Rewrite operators throughout a vl-arguments-p
- Vl-alwayslist-oprewrite
- Rewrite operators throughout a vl-alwayslist-p
- Vl-eventcontrol-oprewrite
- Rewrite operators throughout a vl-eventcontrol-p
- Vl-delaycontrol-oprewrite
- Rewrite operators throughout a vl-delaycontrol-p
- Vl-plainarg-oprewrite
- Rewrite operators throughout a vl-plainarg-p
- Vl-namedarg-oprewrite
- Rewrite operators throughout a vl-namedarg-p
- Vl-modinst-oprewrite
- Rewrite operators throughout a vl-modinst-p
- Vl-maybe-expr-oprewrite
- Rewrite operators throughout a vl-maybe-expr-p
- Vl-initial-oprewrite
- Rewrite operators throughout a vl-initial-p
- Vl-gateinst-oprewrite
- Rewrite operators throughout a vl-gateinst-p
- Vl-assign-oprewrite
- Rewrite operators throughout a vl-assign-p
- Vl-goofymux-p
- Recognize certain special muxes.
- Vl-evatom-oprewrite
- Rewrite operators throughout a vl-evatom-p
- Vl-always-oprewrite
- Rewrite operators throughout a vl-always-p
- Vl-replicate-weirdint-bits
- Generate n copies of a weird integer.
- Vl-maybe-consolidate-multiconcat
- Vl-qmark-p
- Recognize a ? b : c and return the components, or return
nils for each when it's not a ?: expression.
- Vl-goofymux-rewrite
- Annotate weird muxes with less conservative X behavior.
- Vl-module-oprewrite
- Vl-design-oprewrite
- Top-level oprewrite transform.
