• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
      • Svex-simplify
      • Svl-flatten-design
      • Svl-run
        • Svl-run-phase
          • Svl-run-phase-wog
        • Svl-run-phase-wog
      • Svl-run->svex-alist
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svl-run

Svl-run-phase

Run a single phase of svl-run

Signature

(svl-run-phase modname inputs delayed-env modules) 
  → 
(mv out-vals next-delayed-env)

Arguments

modname — Name of the module to run.
    Guard (sv::modname-p modname).

inputs — Values of the inputs as a list.
    Guard (sv::4veclist-p inputs).

delayed-env — Environment from the previos phase for state holding components.
    Guard (svl-env-p delayed-env).

modules — The constant SVL-design instance.
    Guard (svl-module-alist-p modules).

Returns

out-vals — Type (sv::4veclist-p out-vals), given (and (sv::4veclist-p inputs) (svl-env-p delayed-env) (svl-module-alist-p modules)) .

next-delayed-env — Type (svl-env-p next-delayed-env), given (and (sv::4veclist-p inputs) (svl-env-p delayed-env) (svl-module-alist-p modules)) .

The svl-run function operates on phases as defined by the input bindings alits (input simulation pattern). SVL-RUN-PHASE is the function to run each each phase for each module.

'inputs' arguments should be a list of the concrete (for execution) or variables (for proofs). The order of inputs are determined by their order in the SVL-design entry.

'delayed-env' is a special structure for state holding elements. If the user is dealing with sequential circuit designs, then it is recommended to use svl-run instead. svl-run can be used for combinational circuits as well. If you would like to use svl-run-phase on combinational circuits, then you can pass '(nil nil) or (svl::make-svl-env) for delayed-env. This designates empty state.

svl-run-phase might be too slow to use for proofs. You can use svl-run-phase-wog instead, which has the same arguments but no guards.

Subtopics

Svl-run-phase-wog

Same as svl-run-phase but without guards