Defstv
Introduce a symbolic test vector as a constant.
Example:
(defstv my-run
:mod *my-mod*
:inputs '(("opcode" _ _ op _) ...)
:outputs '(("result" _ _ _ _ res _) ...)
:internals '(("foo.bar.mybus" _ _ mb _) ...)
:overrides '(("foo.bar.mywire" _ mw _ _) ...)
:labels '(A nil B nil C nil)]
:parents ...
:short ...
:long ...)
The defstv command is the main interface for defining symbolic test
vectors. It compiles the STV, does the necessary ESIM simulations, and gets
everything ready for stv-run and stv-debug. It generates
convenient macros for use in def-gl-thm commands, and can also produce
xdoc documentation.
Required Arguments
- :mod should be the esim module you want to simulate, and
must be the name of a non-local defconst. This unusual
requirement lets us avoid writing the module into the certificate, which can
significantly improve performance when including books with STVs.
- The :inputs, :outputs, :internals, and :overrides
control how to simulate the module. For the syntax and meaning of these lines,
see symbolic-test-vector-format.
Optional Arguments
- :parents, :short, and :long are as in defxdoc. If
any of these options is given, documentation will be generated for the STV.
This documentation includes a fancy table that shows the simulation.
- :labels are only used for documentation. If they are provided, they
must be a symbol list. These symbols will only be used to label the stages of
the simulation, with nil leaving a blank. (Having the pipe stage names in
the diagram is really nice).
Resulting Functions and Macros
- (my-run)
- This is a disabled 0-ary function (i.e., a constant) that is a processed-stv-p. You should generally only interact with this object using
interfacing functions like stv->vars, stv-out->width, etc., and
not directly use the processed-stv-p accessors (in case we change the
format).
- (my-run-autohyps)
- This is a macro that expands to something like:
(and (unsigned-byte-p 4 opcode)
(unsigned-byte-p 64 abus)
(unsigned-byte-p 64 bbus)
...)
That is, it says each input simulation variable is a natural number of the
proper width. This is generally useful in the :hyp of a def-gl-thm
about your STV.
- (my-run-autoins)
- This is a macro that expands to something like:
(list (cons 'opcode opcode)
(cons 'abus abus)
(cons 'bbus bbus)
...)
That is, it constructs an alist that binds the name of each simulation variable
to the corresponding ACL2 symbol. This is generally useful in the :concl
of a def-gl-thm about your STV, i.e., your conclusion might be something
like:
(b* ((out-alist (stv-run (my-run) (my-run-autoins))))
(outputs-valid-p out-alist))
- (my-run-autobinds)
- This is a macro that expands to something like:
(gl::auto-bindings (:nat opcode 4)
(:nat abus 64)
(:nat bbus 64)
...)
See gl::auto-bindings for some details. This is generally meant to be
used in the :g-bindings of a def-gl-thm about your STV.
- These bindings are probably quite lousy. For instance, if this is
some kind of ALU then we probably want to :mix the abus and
bbus. But the generated bindings just use whatever variable order is
suggested by the initial and input lines, and doesn't smartly mix together
signals.
- If your module is small or you're using gl::gl-satlink-mode, then
this may be fine and very convenient. For more complex modules, you'll
probably want to write your own binding macros. See stv-easy-bindings
for a high-level way to describe most kind of bindings.
- (my-run-mod)
- This is a disabled 0-ary function (i.e., a constant) that either returns
*mod* or, when :overrides are used, some modified version of
*mod* where the overridden wires have been cut. There is ordinarily no
reason to need this, but certain functions like stv-debug make use of
it.
Subtopics
- Defstv-fn
- Implementation of defstv.
- Defstv-main
- Main error checking and processing of an STV.
- Stv-autohyps
- Generate the body for an STV's autohyps macro.
- Stv-autobinds
- Generate the body for an STV's autobinds macro.
- Stv-autoins
- Generate the body for an STV's autoins macro.
