		Search-engine friendly clone of the ACL2 documentation.

Esim-vl

Esim-vl-find-io

Produce an LSB-first list of E wire names corresponding to a particular input or output of the original Verilog module.

(esim-vl-find-io basename pat) returns a vl-emodwirelist-p.

The basename is a string that names a wire in the original Verilog module. The pat should be either the :i or :o of an E module that VL has produced.

Example. If your Verilog module is something like:

module mymodule (o, a, b);
  input [3:0] a;
  input b;
  ...
endmodule

Then the resulting :i pattern for the E module |*mymodule*| should be something like:

:i ((a[0] a[1] a[2] a[3])
    (b))

And here are some examples of using esim-vl-find-io:

(esim-vl-find-io "a" (gpl :i |*mymodule*|)) --> (a[0] a[1] a[2] a[3])
(esim-vl-find-io "b" (gpl :i |*mymodule*|)) --> (b)
(esim-vl-find-io "c" (gpl :i |*mymodule*|)) --> NIL

On success the list of returned bits is non-empty. The least significant bit comes first. NIL indicates that the wire was not found.

If pat is not a valid i/o pattern for an E module produced by VL, i.e., it does not satisfy esim-vl-iopattern-p, a hard error will be caused.

Definitions and Theorems

Function: esim-vl-find-io

(defun
 esim-vl-find-io (basename pat)
 (declare (xargs :guard (stringp basename)))
 (if
  (esim-vl-iopattern-p pat)
  (esim-vl-find-io-main basename pat)
  (er
   hard? 'esim-vl-find-io
   "This doesn't look like a valid I/O pattern for a VL-translated ~
           module: ~x0"
   pat)))

Theorem: vl-emodwirelist-p-of-esim-vl-find-io

(defthm vl-emodwirelist-p-of-esim-vl-find-io
        (vl-emodwirelist-p (esim-vl-find-io basename pat)))

Theorem: true-listp-of-esim-vl-find-io

(defthm true-listp-of-esim-vl-find-io
        (true-listp (esim-vl-find-io basename pat))
        :rule-classes :type-prescription)

Subtopics

Esim-vl-find-io-main: (esim-vl-find-io-main basename x) finds the first iopattern entry in x with this basename.