		Search-engine friendly clone of the ACL2 documentation.

Mlib

Extract-vl-types

Extract Verilog data types to access them with ACL2 functions

Signature:

(extract-vl-types  :design design-name
                   [:module module-name-to-add-to-scope] ;; optional
                   [:parents parents-for-generated-docs] ;; optional
                   ... vl-types: list of datatype/constant/wire names ...)

Example call:

(vl::extract-vl-types  :design *my-good-simplified-svex-design*
                       :module "my_module_name"
                       :parents (my-extracted-vl-types)
                       "my_data_struct" "my_data_struct2")

The above call will generate an event that submits ACL2 accessor, modifier, and debug functions for "my_data_struct", "my_data_struct2", and their children if there are any.

"design" should be the "good" output from vl-design->sv-design stage.
"module" can be nil or a Verilog module name. When nil, the program only searches for globally defined data structures. When non-nil, it searches in the scope of that given module name.
"vl-types" can be a number of Verilog data structures, constants, or wires. The program will generate accessor functions for these data structures as well as their children. These data types can be "struct", "enum", "union", or packed/unpacked vectors. For constants, a defconst event will be submitted. Users may find it useful to pass some wire names in cases they are declared as a vector in the given module.

Accessors

Using the generated functions, users can access a part of a given data structure. For example, if we have a large struct with a lot of fields, say named "t_main", then the program will generate a macro with the same name: |t_main| (reminder: Verilog is case-sensitive and so are our symbol/function names). Say that we have a variable called "main" in our conjectures representing a signal of type "t_main" (assuming we use ACL2::defsvtv). Then, we can access individual fields of this signal using the generated |t_main| macro. For example:

(|t_main| main "data[0].dword[3]")
(|t_main| main "uop.size")

In case of enumarated types, their generator functions can take a string or an integer, and return corresponding integer or string values, respectively.

Modifiers

vl::extract-vl-types will also generate "change" macros for every type. For example:

(change-|t_main| main "data[0].dword[3]" 12)

will set the "data[0].dword[3]" field of main to 12.

More arguments can be passed to change other entries in the same call:

(change-|t_main| main "data[0].dword[3]" 12 "uop.size" 0)

If a field is repeated in the arguments or a field is passed that has an overlap with a previos argument, then the most recent one will override the previous one(s).

Debug Functions

The program will also created "debug" macros/functions for every type. For example:

(|t_main|-debug main)

will return a large term that has all the entries for a given concrete value "main". Arguments to these debug functions are:

A list of fields to exclude from printing. For example:
```
(|t_main|-debug main :exclude ("uop.size"
                               "data[0]"
                               "data[1].dword"
                               "data[2].*"))
```
When there is a ".*" at the end of a skipped argument (e.g., "data[2].*"), then the value of that argument (e.g., "data[2]") will be included but not its fields. Without the ".*", then nothing about that field (e.g., "data[0]") will be included.
A depth limit (natural number). When set to a large number, the debug functions will dive into the children and call the debug functions of all the subfields. Users can set this to a small natural number to limit the depth of the function calls. In that case, the debug functions dive upto the specified level only.
```
(|t_main|-debug main :exclude ("uop.size"
                               "data[2].*")
                     :depth-limit 2)
```

Minimal Non-local Book Inclusion

The extract-vl-types event requires a significant part of the VL library to be loaded, but the generated macros only require a few utilities. Those requirements are included in the book "centaur/vl/mlib/extract-vl-types-support". Therefore, you can do the following in a book if you want to minimize what that book nonlocally includes:

(include-book "centaur/vl/mlib/extract-vl-types-support" :dir :system)
(local (include-book "centaur/vl/mlib/extract-vl-types" :dir :system))

(vl::extract-vl-types ...)

Similarly, vl-extract-types can be used locally to an encapsulate as follows (note the use of make-event to wrap the macro call of extract-vl-types:

(include-book "centaur/vl/mlib/extract-vl-types-support" :dir :system)
(encapsulate nil
  (local (include-book "centaur/vl/mlib/extract-vl-types" :dir :system))
  (make-event '(vl::extract-vl-types ...)))