• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
        • Defstv
        • Stv-compile
          • Stv-expand-input-entry
          • Stv-expand-output-entry
          • Stv-restrict-alist
          • Stv-extraction-alists
          • Stv-expand-input-lines
          • Stv-expand-input-entries
          • Stv-expand-output-entries
          • Stv-expand-internal-lines
          • Stv-expand-output-lines
          • Stv-expand-internal-line
          • Stv-gensyms
          • Stv-forge-state-bit
          • Safe-pairlis-onto-acc
        • Symbolic-test-vector-format
        • Stv-implementation-details
        • Compiled-stv-p
        • Stv-run-for-all-dontcares
        • Stv-run
        • Stv-process
        • Stv-run-check-dontcares
        • Symbolic-test-vector-composition
        • Stv-expand
        • Stv-easy-bindings
        • Stv-debug
        • Stv-run-squash-dontcares
        • Stvdata-p
        • Stv-doc
        • Stv2c
        • Stv-widen
        • Stv-out->width
        • Stv-in->width
        • Stv->outs
        • Stv-number-of-phases
        • Stv->ins
        • Stv-suffix-signals
        • Stv->vars
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Stv-compile

Stv-expand-input-entries

Extend stv-expand-input-entry across a line.

Signature

(stv-expand-input-entries name width 
                          pnum entries gensyms usersyms prev-val) 
 
  → 
(mv new-entries gensyms usersyms)

Arguments

name — Guard (and (atom-listp name) (consp name)).

width — Guard (equal width (len name)).

pnum — Guard (natp pnum).

entries — Guard (true-listp entries).

Definitions and Theorems

Function: stv-expand-input-entries

(defun
    stv-expand-input-entries
    (name width
          pnum entries gensyms usersyms prev-val)
    (declare (xargs :guard (and (and (atom-listp name) (consp name))
                                (natp pnum)
                                (true-listp entries)
                                (equal width (len name)))))
    (let ((__function__ 'stv-expand-input-entries))
         (declare (ignorable __function__))
         (b* (((when (atom entries))
               (mv nil gensyms usersyms))
              ((mv new-car gensyms usersyms)
               (stv-expand-input-entry name width pnum (car entries)
                                       gensyms usersyms prev-val))
              ((mv new-cdr gensyms usersyms)
               (stv-expand-input-entries name width (+ 1 pnum)
                                         (cdr entries)
                                         gensyms usersyms new-car)))
             (mv (cons new-car new-cdr)
                 gensyms usersyms))))

Theorem: stv-expand-input-entries-mvtypes-0

(defthm
 stv-expand-input-entries-mvtypes-0
 (true-listp
  (mv-nth
      0
      (stv-expand-input-entries name width pnum
                                entries gensyms usersyms prev-val)))
 :rule-classes :type-prescription)

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

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