		Search-engine friendly clone of the ACL2 documentation.

Hierarchy

Vl-design-toplevel

(vl-design-toplevel x) gathers the names of any modules or interfaces that are defined but are never instantiated in a design, and returns them as an ordered set.

Signature
(vl-design-toplevel x) → names
Arguments: x — Guard (vl-design-p x).
Returns: names — Type (string-listp names).

Memoized. Cleared in vl-scopestacks-free.

Identifying whether a module/interface is a top-level design element is important for resolving certain hierarchical identifiers and as a starting point for elaboration. See in particular vl-follow-hidexpr and vl-design-elaborate.

Historically we only looked at top level modules and ignored interfaces. We now gather both modules and interfaces that are never used. One nice consequence of this is that it means elaboration won't throw away any unused interfaces, which means we can get their warnings during vl-lint checking.

Note that keeping interfaces here seems to match the behavior of NCVerilog but not VCS. When given code such as:

interface foo ;

  wire ww;

  function bar (input in);
    assign bar = in;
  endfunction

endinterface

module mymod ;

  reg r;
  assign foo.ww = r;
  wire w = foo.bar(r);

  initial begin
    r = 0;
    #10;
    $display("W is %d", w);
    $display("FOO.WW is %d", foo.ww);
  end

endmodule

we find that NCV seems to work fine but VCS reports that interface foo is not instantiated and will be ignored, and then causes ``cross-module reference errors'' that complain about our uses of foo.bar and foo.ww. We haven't tried to deeply look at the SystemVerilog standard to figure out which tool is correct, but it probably doesn't matter much either way.

Definitions and Theorems

Function: vl-design-toplevel

(defun vl-design-toplevel (x)
 (declare (xargs :guard (vl-design-p x)))
 (let ((__function__ 'vl-design-toplevel))
  (declare (ignorable __function__))
  (b*
   (((vl-design x))
    (mentioned
     (union
         (mergesort (vl-modulelist-everinstanced x.mods))
         (mergesort (vl-interfacelist-everinstanced x.interfaces))))
    (defined
        (union (mergesort (vl-modulelist->names x.mods))
               (mergesort (vl-interfacelist->names x.interfaces)))))
   (difference defined mentioned))))

Theorem: string-listp-of-vl-design-toplevel

(defthm string-listp-of-vl-design-toplevel
  (b* ((names (vl-design-toplevel x)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-design-toplevel

(defthm true-listp-of-vl-design-toplevel
  (true-listp (vl-design-toplevel x))
  :rule-classes :type-prescription)

Theorem: setp-of-vl-design-toplevel

(defthm setp-of-vl-design-toplevel
  (setp (vl-design-toplevel x)))

Theorem: vl-design-toplevel-of-vl-design-fix-x

(defthm vl-design-toplevel-of-vl-design-fix-x
  (equal (vl-design-toplevel (vl-design-fix x))
         (vl-design-toplevel x)))

Theorem: vl-design-toplevel-vl-design-equiv-congruence-on-x

(defthm vl-design-toplevel-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-design-toplevel x)
                  (vl-design-toplevel x-equiv)))
  :rule-classes :congruence)