Stv-expand
Expand Verilog-style names throughout an STV into LSB-ordered ESIM
style paths.
- Signature
(stv-expand stv mod) → new-stv
- Arguments
- stv — Guard (stvdata-p stv).
- Returns
- new-stv — Copy of stv but with all names expanded.
Type (stvdata-p new-stv), given the guard.
This is an STV preprocessing step which can be run before or after
stv-widen. It only affects the names in each STV line.
During this step, we resolve Verilog-style names like "foo[3:0]" and
"foo.bar.baz[6:0]," replacing them with LSB-ordered lists of ESIM bits or
paths. This keeps the Verilog-specific stuff out of the rest of the STV
compiler.
Definitions and Theorems
Function: stv-expand
(defun stv-expand (stv mod)
(declare (xargs :guard (stvdata-p stv)))
(let ((__function__ 'stv-expand))
(declare (ignorable __function__))
(b* (((stvdata stv) stv))
(make-stvdata
:inputs (stv-expand-names-in-lines stv.inputs
:i mod)
:outputs (stv-expand-names-in-lines stv.outputs
:o mod)
:internals (stv-expand-hids-in-lines stv.internals mod)
:overrides (stv-expand-hids-in-lines stv.overrides mod)))))
Theorem: stvdata-p-of-stv-expand
(defthm stvdata-p-of-stv-expand
(implies (and (force (stvdata-p stv)))
(b* ((new-stv (stv-expand stv mod)))
(stvdata-p new-stv)))
:rule-classes :rewrite)
Subtopics
- Stv-expand-name
- Expand a name from a symbolic test vector's line into explicit lists
of E bits.
- Stv-hid-parse
- Match a Verilog-style plain or hierarchical name, perhaps with a bit-
or part-select on the end of it.
- Stv-wirename-parse
- Match a Verilog-style wire name, bit-select, or part-select.
- Stv-hid-to-paths
- Convert a Verilog-style plain or hierarchical name (optionally with a
bit- or part-select) into an LSB-ordered list of non-canonical ESIM
paths.
- Stv-maybe-match-select
- Match an expression with an optional bit- or part-select.
- Stv-hid-split
- Splits up a HID into a list of instance names and a wire name.
- Stv-expand-hids-in-lines
- (stv-expand-hids-in-lines lines mod) expands all of the HIDs in a list of
STV internal lines into lists of esim paths.
- Stv-expand-names-in-lines
- Expands all of the names in a list of STV :input or :output lines.
- Stv-expand-hid
- (stv-expand-hid name mod) expands a signal name when it is allowed to be
hierarchical, i.e. a hid or a list of esim paths.
- Stv-check-noncanonical-paths
- Checks that the listed paths all exist in the module
