		Search-engine friendly clone of the ACL2 documentation.

Esim

Defmodules

High level command to load Verilog files, transform them, and generate the corresponding E modules.

Note: if you are new to VL and are trying to load some Verilog modules, you might want to start with the ESIM Hardware Verification Tutorial located in

books/centaur/esim/tutorial/intro.lisp

, which shows some examples of using defmodules and working with the resulting translation.

The defmodules macro allows you to load Verilog files into your ACL2 session "on the fly."

General Form:

(defmodules *name*         ;; a name for this translation
  loadconfig               ;; required, says which files to load
  [:simpconfig simpconfig] ;; optional, simplification options

The required loadconfig is vl-loadconfig-p that says which files to load, which directories to search for modules in, etc. For very simple cases where you just want to load a few self-contained Verilog files, you can just do something like this:

(defmodules *foo*
  (make-vl-loadconfig
    :start-files (list "foo_control.v" "foo_datapath.v")))

After submitting this event, *foo* will be an ACL2 defconst that holds a vl-translation-p object. This object contains the parsed, simplified Verilog modules, their corresponding E modules, etc.

The vl-loadconfig-p has many options for setting up include paths, search paths, search extensions, initial `define settings, etc. For instance, to parse a larger project that makes use of library modules, you might need a command like:

(defmodules *foo*
  (make-vl-loadconfig
    :start-files  (list "foo_control.v" "foo_datapath.v")
    :search-path  (list "/my/project/libs1" "/my/project/libs2" ...)
    :searchext    (list "v" "V")
    :include-dirs (list "./foo_incs1" "./foo_incs2")
    :defines      (vl-make-initial-defines '("NO_ASSERTS" "NEW_CLKTREE"))))

Aside from the load configuration, you can also control certain aspects of how simplification is done with the simpconfig option; see vl-simpconfig-p. In many cases, the defaults will probably be fine.

Subtopics

Vl-translation-p: The result of translating a Verilog or SystemVerilog design.
Vl-simplify: Top level interface for simplifying Verilog modules for use in formal verification with esim.
Defmodules-fn: Load and simplify some modules.