		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm

Defnamemap

Define a mapping between some user-provided names and internal signals of a design, with convenient macros for accessing them and looking them up in environments.

SV designs use fairly verbose and ugly variable names internally. To access signals of a design less painfully, this macro supports the definition of maps from user-provided names to SV-internal signals, with macro support for converting them at translation time and conveniently looking them up in environments.

Usage:

(defnamemap myname
   :design *my-sv-design*
   :names '(("foo.bar[3].baz"    baz3)  ;; Verilog-style signal names paired with user variable names
            ("src_data[1]"       src2)
            ("result_flags[0]"   ie))
   :pkg-sym my-pkg        ;; optional, defaults to basename
   :stobj my-svtv-stobj)  ;; optional, defaults to sv::svtv-data

The invocation above produces three things:

A constant *myname-namemap*, containing the namemap object
A macro myname-sig, which can be invoked as e.g. (myname-sig baz3), which translates to the quoted value that baz3 is mapped to in the namemap
A (see B*) binder myname-sigs that looks up the values of the given signals in an environment (a svex-env object) and binds them to names. For example:
```
(b* (((myname-sigs baz3 (my-src src2)) env))
  (list baz3 my-src))
```
Here the variables baz3 and my-src will be bound to (respectively) the values bound to the SV-internal translations of Verilog signal names "foo.bar[3].baz" and "src_data[0]" in env.

:names syntax

For convenience, this macro supports a few different syntactic forms for the elements of the :names argument:

"verilogname" will use the given string itself as the variable name, mapping that string to the SV-internal translation of it.
(name . "verilogname")
("verilogname" name) (similar to defsvtv$ syntax within :stages
("verilogname" . name)

Additionally, the macro should be able to determine whether the user wanted to evaluate the names or not. E.g., the following three forms should all have the same result:

:names (("foo" bar) ...)
:names '(("foo" bar) ...)
:names (cons (list "foo" 'bar) ...)

Internals

The internal representations of these signals are as lhs objects. An LHS is a fixed-width concatenation of fixed segments of signals. The design hierarchy has to be consulted to determine the particular LHS that a given Verilog-style name maps to. To compute the mapping (in particular, to translate the Verilog-style names to proper SV-internal LHS objects), the design is first flattened and its moddb and aliases mappings are computed. This step can be skipped if it was already done previously and the result stored in the svtv-data stobj, as it would be by (for example) a prior defsvtv$ or defcycle event.

Since the signal names map to LHS objects, the values extracted for them from the environment are computed with lhs-eval-zx. This zero-extends the value of the signal at its width. The following is a possible expansion for the B* binding:

(b* (((myname-sigs baz3 (my-src src2)) env))
  (list baz3 my-src))
-->
(let* ((baz3 (lhs-eval-zx '((5 :VAR ("foo" "bar" 3 . "baz") . 0)) env))
       (my-src (lhs-eval-zx '((64 "src_data" . 64)) env)))
  (list baz3 my-src))