• 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
        • Esim-primitives
        • E-conversion
        • Esim-steps
          • Esim-sexpr-simp-new-probe-steps
          • Esim-sexpr-new-probe-steps
          • Esim-faig-new-probe-steps
          • Esim-sexpr-top-steps
          • Esim-sexpr-simp-steps
          • Esim-sexpr-probe-steps
          • Esim-faig-top-steps
          • Esim-faig-probe-steps
          • Esim-sexpr-steps
          • Esim-faig-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
  • Esim

Esim-steps

Various stepping functions for esim.

Usage

(<step-fn> mod ins st)

where <step-fn> is one of:

  • esim-sexpr-steps
  • esim-sexpr-probe-steps
  • esim-sexpr-top-steps
  • esim-faig-steps
  • esim-faig-probe-steps
  • esim-faig-top-steps

In each case:

  • mod is an esim module
  • ins is a list of alists
  • st is a single alist

These functions all simulate the module for n steps, where n is the length of ins, beginning with initial state st, where the inputs for the k+1st step are given by (nth k ins).

The -sexpr- variants take and produce alists mapping signals to 4v-sexprs.

The -faig- variants take and produce alists mapping signals to faigs.

The -probe- variants produce three outputs, each a list of alists: nsts, outs, and internals. The non-probe variants only produce nsts and outs.

  • nsts is the list of next states, i.e., (nth k nsts) is an alist giving the module state after k+1 steps,
  • outs is the list of outputs, i.e., (nth k outs) gives the outputs from the k+1th step. In the -top- variants only, this will also include the top-level module's internal signals.
  • internals is the list of internal signals, i.e., (nth k internals) gives the internal signal settings after the k+1st step.

Subtopics

Esim-sexpr-simp-new-probe-steps
ESIM stepping function.
Esim-sexpr-new-probe-steps
ESIM stepping function.
Esim-faig-new-probe-steps
ESIM stepping function.
Esim-sexpr-top-steps
ESIM stepping function.
Esim-sexpr-simp-steps
ESIM stepping function.
Esim-sexpr-probe-steps
ESIM stepping function.
Esim-faig-top-steps
ESIM stepping function.
Esim-faig-probe-steps
ESIM stepping function.
Esim-sexpr-steps
ESIM stepping function.
Esim-faig-steps
ESIM stepping function.