|
|
|---|
|
|
|
|---|
Our expressions may involve the application of a fixed set of known functions. There are functions available for modeling many bit-vector operations like bitwise and, plus, less-than, and other kinds of hardware operations like resolving multiple drivers, etc.
SVEX has a fixed language of known functions. The following table shows the function symbols (all in the SV package) and their meanings.
We make no attempt to have a minimal set of functions. Generally speaking, the incremental cost in complexity of supporting more functions is relatively low. Our tools for rewriting and symbolically evaluating expressions can be proven correct, so there is little risk that adding new operations to the backend could cause any problems.
On the other hand, the correct translation from languages like Verilog into SV expressions is a serious concern, and we have no way to prove it is correct. Where possible, then, it seems best to add new operators to the backend to make the translation from Verilog as simple as possible.
| SVEX form | 4vec function | Description |
|---|---|---|
| 4vec-fix | identity function | |
| 4vec-bit-extract | bit select | |
| 3vec-fix | change Z bits to Xes | |
| 4vec-bitnot | bitwise negation | |
| 4vec-bitand | bitwise AND | |
| 4vec-bitor | bitwise OR | |
| 4vec-bitxor | bitwise XOR | |
| 4vec-res | resolve (short together) | |
| 4vec-resand | resolve wired AND | |
| 4vec-resor | resolve wired OR | |
| 4vec-override | resolve different strengths | |
| 4vec-onset | identity, except Z becomes 0 | |
| 4vec-offset | negation, except Z becomes 0 | |
| 4vec-reduction-and | unary (reduction) AND | |
| 4vec-reduction-or | unary (reduction) OR | |
| 4vec-parity | reduction XOR, i.e. parity | |
| 4vec-zero-ext | zero extend | |
| 4vec-sign-ext | sign extend | |
| 4vec-concat | concatenate at a given bit width | |
| 4vec-rev-blocks | reverse order of blocks | |
| 4vec-rsh | right shift | |
| 4vec-lsh | left shift | |
| 4vec-plus | addition | |
| 4vec-minus | subtraction | |
| 4vec-uminus | unary minus | |
| 4vec-times | multiplication | |
| 4vec-quotient | division | |
| 4vec-remainder | modulus | |
| 4vec-xdet | identity on binary vectors, else X | |
| 4vec-countones | count of 1-bits | |
| 4vec-onehot | one-hot check | |
| 4vec-onehot0 | one-hot check (0-hot allowed) | |
| 4vec-< | less than | |
| 4vec-== | equality | |
| 4vec-=== | case equality (scary verilog semantics) | |
| 4vec-===* | modified case equality (x-monotonic if y is constant) | |
| 4vec-wildeq | wildcard equality (scary verilog semantics) | |
| 4vec-wildeq-safe | wildcard equality (X-monotonic version) | |
| 4vec-symwildeq | wildcard equality for casez | |
| 4vec-clog2 | ceiling of log2 | |
| 4vec-pow | exponentiation | |
| 4vec-? | if-then-else | |
| 4vec-?* | if-then-else (for statements) | |
| 4vec-bit? | bitwise if-then-else | |
| 4vec-bit?! | bitwise if-then-else, only chooses then[i] when test[i]===1 | |
| 4vec-?! | procedural if-then-else, only chooses then when test has a definite 1 bit | |
| 4vec-part-select | part select | |
| 4vec-part-install | part install |