|
|
|---|
|
|
|
|---|
Evaluate a symbolic test vector at particular, concrete inputs, and generate a waveform.
(stv-debug pstv
input-alist &key (filename '"stv.debug")
dontcare-ins (default-signal-val ''x)
(viewer '"gtkwave")
(state 'state))
→
(mv out-alist state)This macro is an extended version of stv-run. In addition to building an alist of the output simulation variables, it also writes out a waveform that can be viewed in a VCD viewer. Note that debugging can be slow, especially the first time before things are memoized.
Function:
(defun stv-debug-fn (pstv input-alist filename dontcare-ins default-signal-val viewer state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (processed-stv-p pstv) (stringp filename) (or (stringp viewer) (not viewer))))) (let ((__function__ 'stv-debug)) (declare (ignorable __function__)) (time$ (b* (((processed-stv pstv) pstv) ((compiled-stv cstv) pstv.compiled-stv) (mod-function (intern-in-package-of-symbol (str::cat (symbol-name pstv.name) "-MOD") pstv.name)) ((mv er mod) (magic-ev-fncall mod-function nil state t t)) ((when er) (mv (raise "Error evaluating ~x0 to look up STV module: ~@1." mod-function (if (eq er 't) "t" er)) state)) ((unless (good-esim-modulep mod)) (mv (raise "Error: ~x0 returned a bad ESIM module: ~@1" mod-function (bad-esim-modulep mod)) state)) (snapshots (time$ (stv-make-snapshots pstv mod) :mintime 1/2 :msg "; stv-debug snapshots: ~st sec, ~sa bytes.~%")) (in-usersyms (make-fast-alist cstv.in-usersyms)) (ev-alist (time$ (append (stv-simvar-inputs-to-bits input-alist in-usersyms) dontcare-ins) :mintime 1/2 :msg "; stv-debug ev-alist: ~st sec, ~sa bytes.~%")) ((with-fast ev-alist)) (evaled-out-bits (time$ (make-fast-alist (4v-sexpr-eval-default-alist pstv.relevant-signals ev-alist default-signal-val)) :mintime 1/2 :msg "; stv-debug evaluating sexprs: ~st sec, ~sa bytes.~%")) (evaled-snapshots (time$ (4v-sexpr-eval-default-alists snapshots ev-alist default-signal-val) :mintime 1/2 :msg "; stv-debug evaluating snapshots: ~st sec, ~sa bytes.~%")) (assembled-outs (time$ (stv-assemble-output-alist evaled-out-bits cstv.out-usersyms) :mintime 1/2 :msg "; stv-debug assembling outs: ~st sec, ~sa bytes.~%")) (- (fast-alist-free evaled-out-bits)) ((mv date state) (oslib::date)) (dump (vl2014::vcd-dump-main mod evaled-snapshots date)) ((mv & & state) (assign writes-okp t)) (state (time$ (vl2014::with-ps-file filename (vl2014::vl-ps-update-rchars dump)) :mintime 1/2 :msg "; vcd-dump file generation: ~st seconds, ~sa bytes.~%")) (certifying-book-p (and (boundp-global 'certify-book-info state) (f-get-global 'certify-book-info state))) (- (if (and viewer (not certifying-book-p)) (b* ((cmd (str::cat viewer " " filename))) (cw "; vcd-dump launching \"~s0\".~%" cmd) (tshell-ensure) (tshell-run-background cmd)) nil))) (mv assembled-outs state)) :msg "; stv-debug: ~st sec, ~sa bytes.~%" :mintime 1)))