• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
          • Stv-doc
          • Stv2c
          • Stv-widen
          • Stv-out->width
          • Stv-in->width
          • Stv-number-of-phases
            • Stv-max-phases-in-lines
          • 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
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Symbolic-test-vectors

Stv-number-of-phases

Maximum length of any line of an STV (i.e., how many phases we are going to simulate.

Signature
(stv-number-of-phases stv) → num-phases
Arguments
stv — Guard (stvdata-p stv).
Returns
num-phases — Type (natp num-phases).

Definitions and Theorems

Function: stv-number-of-phases

(defun stv-number-of-phases (stv)
  (declare (xargs :guard (stvdata-p stv)))
  (let ((__function__ 'stv-number-of-phases))
    (declare (ignorable __function__))
    (b* (((stvdata stv) stv))
      (max (stv-max-phases-in-lines stv.inputs)
           (max (stv-max-phases-in-lines stv.outputs)
                (max (stv-max-phases-in-lines stv.internals)
                     (stv-max-phases-in-lines stv.overrides)))))))

Theorem: natp-of-stv-number-of-phases

(defthm natp-of-stv-number-of-phases
  (b* ((num-phases (stv-number-of-phases stv)))
    (natp num-phases))
  :rule-classes :type-prescription)

Subtopics

Stv-max-phases-in-lines