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.
|change Z bits to Xes
|resolve (short together)
|resolve wired AND
|resolve wired OR
|resolve different strengths
|identity, except Z becomes 0
|negation, except Z becomes 0
|unary (reduction) AND
|unary (reduction) OR
|reduction XOR, i.e. parity
|concatenate at a given bit width
|reverse order of blocks
|identity on binary vectors, else X
|count of 1-bits
|one-hot check (0-hot allowed)
|case equality (scary verilog semantics)
|modified case equality (x-monotonic if y is constant)
|wildcard equality (scary verilog semantics)
|wildcard equality (X-monotonic version)
|wildcard equality for casez
|ceiling of log2
|if-then-else (for statements)
|bitwise if-then-else, only chooses then[i] when test[i]===1
|procedural if-then-else, only chooses then when test has a definite 1 bit