• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
          • Defstv
          • Stv-compile
          • Symbolic-test-vector-format
          • Stv-implementation-details
          • Compiled-stv-p
            • Compiled-stv
              • Make-compiled-stv
              • Change-compiled-stv
              • Honsed-compiled-stv
              • Make-honsed-compiled-stv
              • Compiled-stv->restrict-alist
              • Compiled-stv->override-paths
              • Compiled-stv->override-bits
              • Compiled-stv->out-usersyms
              • Compiled-stv->out-extract-alists
              • Compiled-stv->nst-extract-alists
              • Compiled-stv->nphases
              • Compiled-stv->int-extract-alists
              • Compiled-stv->in-usersyms
              • Compiled-stv->expanded-ins
            • 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
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Compiled-stv-p

    Compiled-stv

    Raw constructor for compiled-stv-p structures.

    Syntax:

    (compiled-stv nphases 
                  nst-extract-alists out-extract-alists 
                  int-extract-alists override-bits 
                  restrict-alist in-usersyms out-usersyms 
                  expanded-ins override-paths)

    This is the lowest-level constructor for compiled-stv-p structures. It simply conses together a structure with the specified fields.

    Note: It's generally better to use macros like make-compiled-stv or change-compiled-stv instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

    The compiled-stv-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-compiled-stv instead.

    Definition

    This is an ordinary constructor function introduced by std::defaggregate.

    Function: compiled-stv

    (defun
     compiled-stv
     (nphases nst-extract-alists out-extract-alists
              int-extract-alists override-bits
              restrict-alist in-usersyms out-usersyms
              expanded-ins override-paths)
     (declare (xargs :guard (and (posp nphases)
                                 (true-listp nst-extract-alists)
                                 (true-listp out-extract-alists)
                                 (true-listp int-extract-alists)
                                 (symbol-listp override-bits)
                                 (true-listp override-paths))))
     (cons
      :compiled-stv
      (cons
       (cons 'nphases nphases)
       (cons
        (cons 'nst-extract-alists
              nst-extract-alists)
        (cons
         (cons 'out-extract-alists
               out-extract-alists)
         (cons
          (cons 'int-extract-alists
                int-extract-alists)
          (cons
           (cons 'override-bits override-bits)
           (cons
            (cons 'restrict-alist restrict-alist)
            (cons
                 (cons 'in-usersyms in-usersyms)
                 (cons (cons 'out-usersyms out-usersyms)
                       (cons (cons 'expanded-ins expanded-ins)
                             (cons (cons 'override-paths override-paths)
                                   nil))))))))))))