		Search-engine friendly clone of the ACL2 documentation.

Esim-vl

Esim-vl-iopattern-p

Recognize a good :i or :o pattern for a VL-translated module.

(esim-vl-iopattern-p x) is a basic syntax check to make ensure that x has the proper shape for a :i or :o field of an E module that VL produces.

Basically, VL writes out :i and :o fields for an E module as two-level lists of vl-emodwire-ps. For instance the :i pattern for a module whose input declarations are:

input [3:0] A;
input B;
input [0:3] C;

Should look like this:

:i ((A[0] A[1] A[2] A[3])    ;; lsb first
    (B)
    (C[3] C[2] C[1] C[0]))   ;; lsb first

See e-conversion for details.

We memoize this function to minimize the expense of these checks. Note that esim-vl-iopattern-p is nonrecursive, so we should only need two memo table entries per module, one for the :i and one for the :o entry.

Definitions and Theorems

Function: esim-vl-iopattern-p

(defun esim-vl-iopattern-p (x)
       (declare (xargs :guard t))
       (and (esim-vl-iopattern-entrylist-p x)
            (uniquep (esim-vl-iopattern-entrylist->basenames x))))

Subtopics

Esim-vl-iopattern-entrylist->basenames: (esim-vl-iopattern-entrylist->basenames x) maps esim-vl-iopattern-entry->basename across a list.
Esim-vl-iopattern-entry-p: (esim-vl-iopattern-entry-p x) recognize lists of vl-emodwire-ps like (A[0] A[1] ... A[N]), i.e., non-empty lists of emodwires with the same basenames and unique indices.
Esim-vl-iopattern-entrylist-p: (esim-vl-iopattern-entrylist-p x) recognizes lists where every element satisfies esim-vl-iopattern-entry-p.
Esim-vl-iopattern-entry->basename: (esim-vl-iopattern-entry->basename x) returns the basename that is shared by all the members of a esim-vl-iopattern-entry-p.
All-equalp-of-vl-emodwirelist->basenames: (all-equalp-of-vl-emodwirelist->basenames basename x) ensures that all of the vl-emodwire-ps in x have this basename.