		Search-engine friendly clone of the ACL2 documentation.

Svmods

An svex-based format for expressing a module hierarchy.

See the subtopics for a description of the format. The top-level description of a design is a design object.

Address
Wire: Wire info as stored in an svex module.
Module
Lhs: A shorthand format for an expression consisting of a concatenation of parts of variables.
Path: Type of a path to a wire in svex modules, expressed relative to the local scope.
Svar-add-namespace: Add a namespace to a variable so that it can be referenced from a lower hierarchy level.
Design
Modinst
Lhs-add-namespace
Modalist: An alist mapping modname-p to module-p.
Path-add-namespace
Modname->submodnames
Name: Type of the names of wires, module instances, and namespaces (such as datatype fields).
Constraintlist-addr-p
Svex-alist-addr-p
Svar-map-addr-p
Lhspairs-addr-p
Modname: A type for names of modules and other hierarchical scopes.
Assigns-addr-p
Lhs-addr-p
Lhatom-addr-p
Modhier-list-measure
Attributes: An alist mapping stringp to maybe-svex-p.
Modhier-measure
Modhier-list-measure-aux
Modhier-loopfreelist-p
Modhier-loopfree-p