AstCAwait is only ever uses in statement position, so model it as a
statement. We should never ever have a coroutine that returns a value.
There is no need for it in SV, nor should we rely on it for internals.
Also reworks the fix for V3Life incorrectly constant propagating the
beforeTrig functions (#7072). The property that upsets V3Life is that
a function:
1. Is called from multiple static call sites (multiple AstCCall)
2. Reads model state directly (AstVarRef to non-locals/arguments)
Such function can only be created internally after scheduling (V3Task
throws an unsupported error on a non-inlined function that reads model
state), so added a flag to AstCFunc to mark the dangerous ones for
V3Life.
Many rules in the Dfg Peephole pass check if a node has more than one
sinks. Redundant variables that will ultimately be removed can prevent
these from matching. Remove such variables during the Peeophole pass
itself to enable more matches.
When randc enum variables have user constraints, they go through the
SMT solver path which treats them as unconstrained bitvectors. This
adds implicit enum membership constraints so the solver only produces
valid enum member values.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
When enum variables (rand or randc) are referenced in user constraints,
the constraint solver declares them as unconstrained bitvectors, which
can produce values outside the valid enum range. Add implicit membership
constraints to restrict solver output to valid enum members
(IEEE 1800-2017 §18.4.2).
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This is an attempt to generate an identical trace file scope hierarchy
both with and without -fno-inline. Primarily because it's needed for
testing in upcoming patch, but also improves consitency prior to #7001
This is primarily cleanup, but there are 2 functional changes included:
- It used to accidentally reorder bodies of AstNodeIf that were outside
an AstAlways. Now it will not touch anything outside an AstAlways.
- Removed one redundant edge from the graph which perturbs the result of
V3Graph::acyclic. This should make no difference for the actual
intended result of reordering NBAs to eliminate shadow variables.
Add a new Dfg pass 'pushDownSel'. This will try to move selects through
a tree of concatenations in order to eliminate temporary nodes holding
intermediate concatenation results. This can get rid of a lot of
variables when packed arrays are assigned in parts (e.g. bit-wise).
Use uint32_t max value instead of zero as sentinel value for a trace
code being unassigned. Prep for follow on patch.
Note the actual trace file will still start codes from one, the codes
in the model are just an offset from the base code.
Yilou Wang
Geza Lore
Igor Zaworski
Geza Lore
Pawel Kojma
Wilson Snyder
Veripool API Bot
Yilou Wang
Todd Strader
Ryszard Rozak
github action
Leela Pakanati