Extract Verilog data types to access them with ACL2 functions
(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 ...)
(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.
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.dword") (|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.
vl::extract-vl-types will also generate "change" macros for every type. For example:
(change-|t_main| main "data.dword" 12)
will set the "data.dword" field of main to 12.
More arguments can be passed to change other entries in the same call:
(change-|t_main| main "data.dword" 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).
The program will also created "debug" macros/functions for every type. For example:
will return a large term that has all the entries for a given concrete value "main". Arguments to these debug functions are:
(|t_main|-debug main :exclude ("uop.size" "data" "data.dword" "data.*"))When there is a ".*" at the end of a skipped argument (e.g., "data.*"), then the value of that argument (e.g., "data") will be included but not its fields. Without the ".*", then nothing about that field (e.g., "data") will be included.
(|t_main|-debug main :exclude ("uop.size" "data.*") :depth-limit 2)