• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
        • Fast-canonicalize-path
        • Extend-internal-paths
        • Follow-esim-path
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Esim

Mod-internal-paths

(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[54]|)

In this example, |core0|, |rf_instd|, and |vl_mux_168| are instance names, whereas |sbar_b[54]| is a wire name. The Verilog syntax for referring to such a wire would be:

core0.rf_instd.vl_mux_168.sbar_b[54]

We memoize both mod-internal-paths and occ-internal-paths since they both involve a good deal of consing. Our original version of this function created symbols like |core0/rf_instd/vl_mux_168/sbar_b[54]| instead of paths (lists of symbols), but that approach had poor performance due to the amounts of string manipulation and interning required. We now just cons together instance and wire names to create paths, which is much faster.

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 |sbar_b[54]| is an internal wire (not an input or output) of the module in which it resides.

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.

Definitions and Theorems

Function: mod-internal-paths

(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)))))

Function: occ-internal-paths

(defun occ-internal-paths (occ)
       (declare (xargs :guard t))
       (extend-internal-paths (gpl :u occ)
                              (mod-internal-paths (gpl :op occ))))

Function: occs-internal-paths

(defun occs-internal-paths (occs)
       (declare (xargs :guard t))
       (if (atom occs)
           nil
           (append (occ-internal-paths (car occs))
                   (occs-internal-paths (cdr occs)))))

Subtopics

Fast-canonicalize-path

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

Extend-internal-paths

(extend-internal-paths a x) constructs a new list where a has been consed onto each element of x.

Follow-esim-path

Walk down a list of instance names (or a path) and retrieve the ESIM module it points to.