		Search-engine friendly clone of the ACL2 documentation.

Mod-internal-paths

Fast-canonicalize-path

(fast-canonicalize-path path mod) produces the canonical version of a path to an internal wire in a module.

Signature: (fast-canonicalize-path path mod) returns (mv successp new-path). On success, new-path is a member of one of the following:

(mod-internal-paths mod)
(gpl :i mod), or
(gpl :o mod).

To understand this function, note that the set of mod-internal-paths does not include any non-canonical paths (inputs or outputs of the target module). For instance, if we have in Verilog something like:

my_mux2 result_mux (.o(main_result), ...)

Then a path such as:

(|foo| |bar| |baz| |result_mux| . |o|)

is not regarded as canonical and will not be included among the internal signals alist produced esim's new-probe mode. However, if we assume that main_result is not one of the inputs or outputs of foo.bar.baz, then the following path is canonical and it is equivalent in that it describes the same wire:

(|foo| |bar| |baz| . |main_result|)

Fast-canonicalize-path should be given a valid path in the sense of mod-all-paths, and tries to return the canonical equivalent. Failure indicates that the given path is invalid, but we do only minimal error checking. In other words, you should not rely on this function to see whether a path is valid.

Definitions and Theorems

Function: fast-canonicalize-path

(defun fast-canonicalize-path (path mod)
 "Returns (MV SUCCESSP NEW-PATH)"
 (declare (xargs :guard (good-esim-modulep mod)))
 (b*
  (((when (atom path)) (mv t path))
   (head (car path))
   (occ (cdr (hons-get head (make-fast-alist (occmap mod)))))
   ((unless occ) (mv nil nil))
   (op (gpl :op occ))
   ((mv tail-successp new-tail)
    (fast-canonicalize-path (cdr path) op))
   ((unless tail-successp) (mv nil nil))
   (tail-inputp (and (atom new-tail)
                     (member-of-pat-flatten new-tail (gpl :i op))))
   (tail-outputp (and (atom new-tail)
                      (not tail-inputp)
                      (member-of-pat-flatten new-tail (gpl :o op))))
   ((when tail-inputp)
    (mv t
        (cdr (assoc-pat->al new-tail (gpl :i op)
                            (gpl :i occ)))))
   ((when tail-outputp)
    (mv t
        (cdr (assoc-pat->al new-tail (gpl :o op)
                            (gpl :o occ))))))
  (mv t (hons head new-tail))))