		Search-engine friendly clone of the ACL2 documentation.

Svtv

Svtv-chase

(Deprecated) Diagnose hardware or stimulus bugs by studying an SVTV run in a special-purpose read-eval-print loop.

Signature
(svtv-chase x env &key (debugdata 'debugdata) (moddb 'moddb) (aliases 'aliases) (svtv-chase-data 'svtv-chase-data) (state 'state) (rewrite 't)) → (mv new-debugdata new-moddb new-aliases new-svtv-chase-data new-state)
Arguments: x — Guard (svtv-p x).; env — Guard (svex-env-p env).; moddb — Guard (moddb-ok moddb).

This version of the utility is deprecated in favor of svtv-chase$.

To enter this read-eval-print loop for the first time, run:

(svtv-chase svtv env)

where SVTV is an svtv object (as produced by defsvtv) and env is an assignment to the input/override signals of that SVTV. Depending on the complexity of the SVTV, the initial setup done by this command may take a few minutes.

When setup is complete, you'll be shown an SVTV-CHASE > prompt. Typing ? at this prompt shows the commands that may be used there. Typically you'll start by going to a signal of interest at a certain phase, using the G command. At a given signal/phase, SVTV-CHASE will print the type of signal -- primary input, initial state, previous state, or internal signal. For internal signals, it will also print the list of signals that are this signal's immediate dependencies. To see the expression driving the current signal, you may enter EXPR. The next step is usually to select one of the signal's dependencies and go to it, by typing its number. To go back to the signal you just left, you may type B to pop the stack of signal/phase positions.

At some point you may want to exit the read-eval-print loop, which you can do by typing X at the prompt. To re-enter the loop, you can skip the initial setup by running (svtv-chase-repl). You may also skip much of the setup but change the input assignment by running (svtv-chase-update env).

Definitions and Theorems

Function: svtv-chase-fn

(defun svtv-chase-fn (x env debugdata moddb
                        aliases svtv-chase-data state rewrite)
 (declare
    (xargs :stobjs (debugdata moddb aliases svtv-chase-data state)))
 (declare (xargs :guard (and (svtv-p x)
                             (svex-env-p env)
                             (moddb-ok moddb))))
 (declare (xargs :guard (open-input-channel-p *standard-oi*
                                              :object state)))
 (let ((__function__ 'svtv-chase))
  (declare (ignorable __function__))
  (b*
   (((svtv x))
    (mod-fn
      (intern-in-package-of-symbol (cat (symbol-name x.name) "-MOD")
                                   x.name))
    ((mv err design)
     (magic-ev-fncall mod-fn nil state t t))
    ((when err)
     (cw! "Couldn't run ~x0: ~@1~%" mod-fn err)
     (mv debugdata
         moddb aliases svtv-chase-data state))
    ((unless (and (design-p design)
                  (modalist-addr-p (design->modalist design))))
     (cw! "~x0 returned a malformed design~%"
          mod-fn)
     (mv debugdata
         moddb aliases svtv-chase-data state))
    ((mv err moddb aliases debugdata)
     (svtv-debug-init design))
    ((when err)
     (mv debugdata
         moddb aliases svtv-chase-data state))
    (debugdata (svtv-debug-set-svtv x
                                    :rewrite rewrite))
    ((mv err namemap probes)
     (svtv-chase-probes x (debugdata->modidx debugdata)
                        moddb aliases))
    (svtv-chase-data
     (if err
      (prog2$
       (cw
        "Svtv-chase: failed to convert ~
                                         outputs to signals--- the '~x0' ~
                                         directive will not be available.  ~
                                         Error: ~@1"
        '(o name)
        err)
       svtv-chase-data)
      (b*
       ((svtv-chase-data
            (set-svtv-chase-data->namemap namemap svtv-chase-data)))
       (set-svtv-chase-data->probes probes svtv-chase-data))))
    ((mv svtv-chase-data state)
     (svtv-chase-update env)))
   (mv debugdata
       moddb aliases svtv-chase-data state))))

Subtopics

Svtv-chase-update: Re-enter the svtv-chase read-eval-print loop, updating the environment but keeping the same SVTV.
Svtv-chase-repl1: Re-enter the svtv-chase read-eval-print loop, with no change to the environment or SVTV.