		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-expand-input-entry

Convert a single user-level input value (e.g., 17, X, abus, etc) into a list of 4v-sexprs.

Signature
(stv-expand-input-entry name width pnum entry gensyms usersyms prev-val) → (mv new-val gensyms usersyms)
Arguments: name — The name of this input, and 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 (atom-listp name) (consp name)).; width — Just the pre-computed width of this input.
Guard (equal width (len name)).; pnum — The current phase number (and starts at 0). We use this to know what suffix to put onto the generated variable names for _ values, e.g., |foo[0].P4|.
Guard (natp pnum).; entry — The actual entry we are trying to expand. For instance, it might be 5, :ones, _, or whatever else the user wrote down for this input at this phase number.; gensyms — A flat list of all the names we have generated so far for _ entries, which we may extend. This allows us to check for name collisions later on.; usersyms — A fast alist that binds the names of simulation variables like opcode to lists of bits that we generate for these symbols, i.e., (opcode[0] ... opcode[n]). This allows us to check for name collisions with generated symbols and width mismatches. That is, we will allow the same variable to be given to multiple inputs at multiple phases, but for that to be sensible these inputs had better have the same width.; prev-val — The sexpr list that this signal expanded to in the previous phase, or NIL if this is the first phase of the simulation. We use this to figure out the new value of a ~ entry.

This function basically defines what each value in an :input line means. We transform each such value into a list of 4v-sexprs. These are the sexprs that will be given to this input during this phase. At a high level, our expansion strategy is:

NAT. Expands to a list of *4vt-sexpr* and *4vf-sexpr*'s, in LSB order, of the appropriate width.
X. Expands to a list of *4vx-sexpr* of the appropriate width.
:ONES. Expands to a list of *4vt-sexpr* of the appropriate width.
~. Expands to a singleton list whose one entry is either *4vf-sexpr* or *4vt-sexpr*, based on the previous value for this signal.
_. Expands to a list of variables, whose names are derived from the names of input bits for this line. Basically, |foo[0]| gets turned into |foo[0].P4| in the 4th phase, etc.
Simulation variables. A simulation variable like opcode is turned into a list like (|opcode[0]| ... |opcode[n]|).

Definitions and Theorems

Function: stv-expand-input-entry

(defun
 stv-expand-input-entry
 (name width
       pnum entry gensyms usersyms prev-val)
 (declare (xargs :guard (and (and (atom-listp name) (consp name))
                             (natp pnum)
                             (equal width (len name)))))
 (let
  ((__function__ 'stv-expand-input-entry))
  (declare (ignorable __function__))
  (b*
   (((when (natp entry))
     (or
      (< entry (ash 1 width))
      (raise
       "Phase ~x0 for ~x1: value ~x2 is too wide to fit in ~x3 ~
                    bits!"
       pnum name entry width))
     (mv (bool-to-4v-sexpr-lst (int-to-v entry width))
         gensyms usersyms))
    ((when (eq entry 'x))
     (mv (replicate width *4vx-sexpr*)
         gensyms usersyms))
    ((when (eq entry :ones))
     (mv (replicate width *4vt-sexpr*)
         gensyms usersyms))
    ((when (eq entry '~))
     (or
      (= width 1)
      (raise
       "Phase ~x0 for ~x1: value ~~ is not legal here.  It can ~
                    only be used in one-bit inputs, but this input is ~x2 ~
                    bits wide."
       pnum name width))
     (or
      prev-val
      (raise
       "Phase ~x0 for ~x1: value ~~ is not legal here.  It must ~
                    be preceeded by a constant true or false, so it cannot be ~
                    used at the start of a line."
       pnum name))
     (or
      (equal prev-val (list *4vt-sexpr*))
      (equal prev-val (list *4vf-sexpr*))
      (raise
       "Phase ~x0 for ~x1: value ~~ is not legal here.  It must ~
                    be preceeded by a constant true or false, but the ~
                    previous value was ~x2."
       pnum name prev-val))
     (mv (if (equal prev-val (list *4vt-sexpr*))
             (list *4vf-sexpr*)
             (list *4vt-sexpr*))
         gensyms usersyms))
    ((when (eq entry '_))
     (let
      ((my-syms
           (stv-suffix-signals name
                               (str::cat ".P" (str::natstr pnum)))))
      (mv my-syms (append my-syms gensyms)
          usersyms)))
    ((unless (and (symbolp entry)
                  (not (keywordp entry))))
     (raise
      "Phase ~x0 for ~x1: value ~x2 is not legal for input lines of ~
                symbolic test vectors.  See :xdoc symbolic-test-vector-format ~
                for help."
      pnum name entry)
     (mv (replicate width *4vx-sexpr*)
         gensyms usersyms))
    (my-syms (stv-gensyms (symbol-name entry) width))
    (look (hons-get entry usersyms)))
   (or
    (not look)
    (equal (cdr look) my-syms)
    (raise
     "Phase ~x0 for ~x1: variable ~x2 cannnot be used here.  This ~
                input is ~x3 bits wide, but ~x2 was previously used for a ~
                ~x4-bit input."
     pnum name entry width (len (cdr look))))
   (mv my-syms gensyms
       (if look usersyms
           (hons-acons entry my-syms usersyms))))))

Theorem: true-listp-of-stv-expand-input-entry-gensyms

(defthm
 true-listp-of-stv-expand-input-entry-gensyms
 (implies
  (true-listp gensyms)
  (b*
   (((mv ?new-val gensyms ?usersyms)
     (stv-expand-input-entry name width
                             pnum entry gensyms usersyms prev-val)))
   (true-listp gensyms))))