• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
            • Honsed-stvdata
            • Make-honsed-stvdata
            • Stvdata->overrides
            • Stvdata->outputs
            • Stvdata->internals
            • Stvdata->inputs
          • Stv-doc
          • Stv2c
          • Stv-widen
          • Stv-out->width
          • Stv-in->width
          • Stv-number-of-phases
          • Stv->outs
          • 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
    • Math
    • Testing-utilities
  • Symbolic-test-vectors

Stvdata-p

Temporary internal representation of STV lines during compilation.

(stvdata-p x) is a std::defaggregate of the following fields.

  • inputs — Invariant (true-list-listp inputs).
  • outputs — Invariant (true-list-listp outputs).
  • internals — Invariant (true-list-listp internals).
  • overrides — Invariant (true-list-listp overrides).

Source link: stvdata-p

Subtopics

Stvdata
Raw constructor for stvdata-p structures.
Make-stvdata
Constructor macro for stvdata-p structures.
Change-stvdata
A copying macro that lets you create new stvdata-p structures, based on existing structures.
Honsed-stvdata
Raw constructor for honsed stvdata-p structures.
Make-honsed-stvdata
Constructor macro for honsed stvdata-p structures.
Stvdata->overrides
Access the overrides field of a stvdata-p structure.
Stvdata->outputs
Access the outputs field of a stvdata-p structure.
Stvdata->internals
Access the internals field of a stvdata-p structure.
Stvdata->inputs
Access the inputs field of a stvdata-p structure.