• 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
          • 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
            • Stvdata
              • Make-stvdata
              • Change-stvdata
              • Make-honsed-stvdata
              • Honsed-stvdata
              • Stvdata->overrides
              • Stvdata->outputs
              • Stvdata->internals
              • Stvdata->inputs
            • 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
    • Stvdata-p

    Stvdata

    Raw constructor for stvdata-p structures.

    Syntax:

    (stvdata inputs outputs internals overrides)

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

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

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

    Definition

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

    Function: stvdata

    (defun
      stvdata
      (inputs outputs internals overrides)
      (declare (xargs :guard (and (true-list-listp inputs)
                                  (true-list-listp outputs)
                                  (true-list-listp internals)
                                  (true-list-listp overrides))))
      (cons :stvdata (cons (cons 'inputs inputs)
                           (cons (cons 'outputs outputs)
                                 (cons (cons 'internals internals)
                                       (cons (cons 'overrides overrides)
                                             nil))))))