Stv-expand-output-entry
Convert a single user-level output/internal value (e.g., _, result)
into a list of 4v-sexprs.
- Signature
(stv-expand-output-entry name width pnum entry usersyms)
→
(mv new-val usersyms)
- Arguments
- name — The name of this output. It should be a list of E input bits in
lsb-first order. That is, Verilog-style names should have already
been expanded away using stv-expand.
Guard (and (true-listp name) (consp name)).
- width — Just the pre-computed width of this output. It must be exactly
equal to (len name). This lets us know how many variables to
generate when we hit a simulation variable.
Guard (equal width (len name)).
- pnum — The current phase number (and starts at 0). This is semantically
irrelevant; we use it only to generate better error messages.
Guard (natp pnum).
- entry — The actual entry we are trying to expand, i.e., it's what the user
wrote down for this output at this phase. To be well-formed, the
entry needs to be _ or a simulation variable, but the user can
write down anything so we have to check that it is valid.
- usersyms — A fast alist binding simulation variables to the lists of bits
that we've generated to represent them. We assume this only
contains the output simulation variables. This lets us make sure
that output variables aren't being reused.
The only valid entries for output lines are _ (for signals we
don't care about) and simulation variables. Here, we just leave any _
values alone, but we replace simulation variables with lists of new variables
that we generate from their names. That is, a simulation variable like
result will be converted into a list of bits like (result[0]
... result[4]).
Definitions and Theorems
Function: stv-expand-output-entry
(defun stv-expand-output-entry (name width pnum entry usersyms)
(declare (xargs :guard (and (and (true-listp name) (consp name))
(natp pnum)
(equal width (len name)))))
(let ((__function__ 'stv-expand-output-entry))
(declare (ignorable __function__))
(b*
(((when (or (natp entry)
(eq entry 'x)
(eq entry '~)
(keywordp entry)
(not (symbolp entry))))
(raise
"Phase ~x0 for ~x1: value ~x2 is not legal for :output lines."
pnum name entry)
(mv nil usersyms))
((when (eq entry '_))
(mv entry usersyms))
(look (hons-get entry usersyms))
((when look)
(raise
"Phase ~x0 for ~x1: variable ~x2 is already in use, so it ~
cannot be used again."
pnum name entry)
(mv nil usersyms))
(my-syms (stv-gensyms (symbol-name entry) width))
(usersyms (hons-acons entry my-syms usersyms)))
(mv my-syms usersyms))))
