• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
          • Unparameterization
          • Elaborate
          • Addnames
          • Annotate
            • Increment-elim
            • Make-implicit-wires
            • Basic-bind-elim
            • Argresolve
            • Basicsanity
              • Vl-interfacelist-basicsanity
              • Vl-modport-portlist->names
              • Vl-modulelist-basicsanity
              • Vl-modport-portlist-check-wellformed
              • Vl-modport-port-check-wellformed
              • Vl-interface-check-modinst-is-subinterface
              • Vl-interface-check-modinsts-are-subinterfaces
              • Vl-modport-portcheck
              • Vl-modportlist-portcheck
              • Vl-interface-basicsanity
              • Vl-port-check-style
              • Vl-portlist-check-style
              • Vl-module-basicsanity
              • Vl-portlist-check-wellformed
              • Vl-port-check-wellformed
              • Vl-design-basicsanity
              • Vl-pps-expr-elided
            • Portdecl-sign
            • Enum-names
            • Port-resolve
            • Udp-elim
            • Vl-annotate-design
            • Vl-annotate-module
          • Clean-warnings
          • Eliminitial
          • Custom-transform-hooks
          • Problem-modules
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Annotate

Basicsanity

Basic sanity checking of various constructs.

This is a set of basic but rather ad-hoc sanity checks that don't really fit into other places. It is carried out as part of annotate. Some of the things we do here...

Port sanity checking

We check that ports satisfy basic well-formedness conditions and agree with its port declarations and to issue style warnings for tricky ports. This is meant to identify cases such as:

module foo (o, a, b);              |   module bar (o, a, b);
  output o;                        |     output o;
  input a;                         |     input c;    // oops, no such port
  // oops, no declaration for b    |     ...
endmodule                          |   endmodule

This is mostly straightforward. One complication is that ports can have many names internally, for instance:

module baz (o, a, .foo( {b, c} ), d) ;
  ...
endmodule

So, in general, we need to gather the names from the port expressions. While we're at it we may issue various port style warnings.

Port and modport name clashes

Most name clash checking for real scopes is done by shadowcheck, but things like the external port names for a module, e.g., the a1 and a2 in

module foo (.a1(b1), .a2(b2)) ;
 ...
endmodule

aren't separate from other scopes, so we check them here. We similarly check the external names listed by modports.

Interface instances

SystemVerilog 25.3 (page 713) prohibits interfaces from instantiating submodules, but interfaces are allowed to instantiate other interfaces. Since we can't tell until after parsing whether a particular instance refers to a module, interface, or user-defined primitive and use the same representation for all of these, we check here that any such instances really do refer to interfaces.

Subtopics

Vl-interfacelist-basicsanity
(vl-interfacelist-basicsanity x ss) maps vl-interface-basicsanity across a list.
Vl-modport-portlist->names
(vl-modport-portlist->names x) maps vl-modport-port->name across a list.
Vl-modulelist-basicsanity
(vl-modulelist-basicsanity x) maps vl-module-basicsanity across a list.
Vl-modport-portlist-check-wellformed
Vl-modport-port-check-wellformed
Vl-interface-check-modinst-is-subinterface
Vl-interface-check-modinsts-are-subinterfaces
Vl-modport-portcheck
Vl-modportlist-portcheck
Vl-interface-basicsanity
Vl-port-check-style
Vl-portlist-check-style
Vl-module-basicsanity
Vl-portlist-check-wellformed
Vl-port-check-wellformed
Vl-design-basicsanity
Top-level basicsanity check.
Vl-pps-expr-elided