(mod-internal-paths mod) produces a list of paths that describe the canonical internal wires in a module.
An example of a "path" is:
(|core0| |rf_instd| |vl_mux_168| . |sbar_b|)
In this example,
We memoize both
We say that a path is canonical when it does not lead to an input or
output of the target module. That is, the above path is canonical exactly if
We produce only canonical paths, because it greatly reduces the number of paths we need to construct. Given some non-canonical path, it is possible to canonicalize it discover its canonical version, see for instance fast-canonicalize-path.
(defun mod-internal-paths (mod) (declare (xargs :guard t)) (let ((local-wires (hons-set-diff (driven-signals mod) (pat-flatten1 (gpl :o mod))))) (append local-wires (occs-internal-paths (gpl :occs mod)))))
(defun occ-internal-paths (occ) (declare (xargs :guard t)) (extend-internal-paths (gpl :u occ) (mod-internal-paths (gpl :op occ))))
(defun occs-internal-paths (occs) (declare (xargs :guard t)) (if (atom occs) nil (append (occ-internal-paths (car occs)) (occs-internal-paths (cdr occs)))))