Svtv-debug-run
- Signature
(svtv-debug-run inalist
&key (filename '"svtv-debug.vcd")
(moddb 'moddb)
(aliases 'aliases)
(debugdata 'debugdata)
(vcd-wiremap 'vcd-wiremap)
(vcd-vals 'vcd-vals)
(state 'state))
→
(mv vcd-wiremap vcd-vals state)- Arguments
- inalist — Guard (svex-env-p inalist).
- filename — Guard (stringp filename).
Definitions and Theorems
Function: svtv-debug-run-fn
(defun svtv-debug-run-fn
(inalist filename moddb aliases
debugdata vcd-wiremap vcd-vals state)
(declare
(xargs :stobjs (moddb aliases
debugdata vcd-wiremap vcd-vals state)))
(declare (xargs :guard (and (svex-env-p inalist)
(stringp filename))))
(let ((__function__ 'svtv-debug-run))
(declare (ignorable __function__))
(svtv-debug-run-logic inalist
:filename filename
:moddb moddb
:aliases aliases
:debugdata debugdata
:vcd-wiremap vcd-wiremap
:vcd-vals vcd-vals)))
