• 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
            • Vl-convert-namedargs
            • Vl-unhierarchicalize-interfaceport
              • Vl-hidexpr-split-right
              • Vl-scopeexpr-split-right
            • Vl-interfacelist-argresolve
            • Vl-modulelist-argresolve
            • Vl-gateinst-dirassign
            • Vl-arguments-argresolve
            • Vl-unhierarchicalize-interfaceports
            • Vl-check-blankargs
            • Vl-annotate-plainargs
            • Vl-modinst-maybe-argresolve
            • Vl-modinst-argresolve
            • Vl-modinstlist-argresolve
            • Vl-gateinstlist-dirassign
            • Vl-interface-argresolve
            • Vl-module-argresolve
            • Vl-namedarglist-alist
            • Vl-make-namedarg-alist
            • Vl-design-argresolve
            • Vl-fast-find-namedarg
            • Vl-namedarg-alist
            • Vl-scopeitem-modport-p
            • Vl-scopeitem-modinst-p
            • Vl-scopeitem-interfaceport-p
            • Vl-port-interface-p
          • Basicsanity
          • 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

• Argresolve

Vl-unhierarchicalize-interfaceport

Sanity check and normalize interface port arguments by dropping hierarchical modinst name components, e.g., transform mypipe.producer to just mypipe.

Signature

(vl-unhierarchicalize-interfaceport arg port ss inst warnings) 
  → 
(mv warnings new-arg)

Arguments

arg — Actual for this port.
    Guard (vl-plainarg-p arg).

port — Corresponding port; not necessarily an interface port.
    Guard (vl-port-p port).

ss — Guard (vl-scopestack-p ss).

inst — The module instance itself, context for error messages.
    Guard (vl-modinst-p inst).

warnings — Guard (vl-warninglist-p warnings).

Returns

warnings — Type (vl-warninglist-p warnings).

new-arg — If arg is of the form myinterface.myport and everything is OK, this will just be myinterface. In any other case, we just return arg unchanged.
    Type (vl-plainarg-p new-arg).

See SystemVerilog-2012 Section 25.5, especially at the top of Page 718. Suppose we have an interface called IPipe with modports named producer and consumer. The names of these modport declarations can be used in two distinct places:

module fooBuilder( IPipe.producer pipe ) ;  // <-- .producer used in the module's port
  ...
endmodule

module top ;
  IPipe mypipe;
  fooBuilder prod ( mypipe.producer );   // <-- .producer used in module instance
endmodule

Our goal here is to deal with the latter kind of usage. The basic idea is to reduce such an argument to just mypipe, after checking that its interface is compatible with the module's interface declaration. This way, later VL code for dealing with interface ports doesn't have to think about hierarchical identifiers that point at modports.

Definitions and Theorems

Function: vl-unhierarchicalize-interfaceport

(defun vl-unhierarchicalize-interfaceport
       (arg port ss inst warnings)
 (declare (xargs :guard (and (vl-plainarg-p arg)
                             (vl-port-p port)
                             (vl-scopestack-p ss)
                             (vl-modinst-p inst)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-unhierarchicalize-interfaceport))
  (declare (ignorable __function__))
  (b*
   ((port (vl-port-fix port))
    ((vl-plainarg arg)
     (vl-plainarg-fix arg))
    ((vl-modinst inst)
     (vl-modinst-fix inst))
    ((unless (vl-port-interface-p port))
     (mv (ok) arg))
    ((vl-interfaceport port))
    (expr (vl-plainarg->expr arg))
    ((unless expr)
     (mv (fatal :type :vl-instance-blank-interface-port
                :msg "~a0: interface port ~s1 is blank."
                :args (list inst port.name))
         arg))
    ((unless (vl-expr-case expr :vl-index))
     (mv
      (fatal
        :type :vl-instance-interface-port-bad-connection
        :msg
        "~a0: interface port argument isn't an interface: .~s1(~a2)"
        :args (list inst port.name expr))
      arg))
    ((vl-index expr))
    ((mv err trace ?context tail)
     (vl-follow-scopeexpr expr.scope ss
                          :strictp nil))
    ((when err)
     (mv
      (fatal
       :type :vl-instance-interface-port-unresolved
       :msg
       "~a0: error resolving interface port argument .~s1(~a2): ~@3"
       :args (list inst port.name expr err))
      arg))
    ((vl-hidstep step1) (first trace))
    ((when (vl-scopeitem-modinst-p step1.item))
     (b*
      (((vl-modinst step1.item))
       (iface (vl-scopestack-find-definition step1.item.modname ss))
       ((unless (and iface (vl-scopedef-interface-p iface)))
        (mv
         (fatal
          :type :vl-instance-interface-port-bad-connection
          :msg
          "~a0: interface port argument isn't an interface: .~s1(~a2)"
          :args (list inst port.name expr))
         arg))
       ((unless (equal step1.item.modname port.ifname))
        (mv
         (fatal
          :type :vl-instance-interface-port-bad-connection
          :msg
          "~a0: type error: interface port ~s1 (type ~s2) ~
                               is connected to ~a3 (type ~s4)."
          :args (list inst port.name
                      port.ifname expr step1.item.modname))
         arg)))
      (mv (ok) arg)))
    ((when (vl-scopeitem-interfaceport-p step1.item))
     (b*
      (((vl-interfaceport step1.item))
       ((unless (equal step1.item.ifname port.ifname))
        (mv
         (fatal
          :type :vl-instance-interface-port-bad-connection
          :msg
          "~a0: type error: interface port ~s1 (type ~s2) ~
                               is connected to ~a3 (type ~s4)."
          :args (list inst port.name
                      port.ifname expr step1.item.ifname))
         arg)))
      (mv (ok) arg)))
    ((unless (vl-scopeitem-modport-p step1.item))
     (mv
      (fatal
        :type :vl-instance-interface-port-bad-connection
        :msg
        "~a0: interface port argument isn't an interface: .~s1(~a2)"
        :args (list inst port.name expr))
      arg))
    ((when (or (consp expr.indices)
               (not (vl-partselect-case expr.part :none))))
     (mv
      (fatal
        :type :vl-instance-modport-indexing
        :msg
        "~a0: array indexing can't be applied to modport: .~s1(~a2)"
        :args (list inst port.name expr))
      arg))
    ((vl-modport step1.item))
    ((unless (vl-hidexpr-case tail :end))
     (mv
      (fatal
       :type :vl-instance-modport-indexing
       :msg
       "~a0: error resolving interface port argument .~s1(~a2): ~
                         trying to index through modport ~s3 with ~a4."
       :args (list inst
                   port.name expr step1.item.name tail))
      arg))
    ((unless (consp (cdr trace)))
     (mv
      (fatal
        :type :vl-instance-interface-port-bad-connection
        :msg
        "~a0: interface port argument isn't an interface: .~s1(~a2)"
        :args (list inst port.name expr))
      arg))
    ((vl-hidstep step2) (second trace))
    ((unless (vl-scopeitem-modinst-p step2.item))
     (mv
      (fatal
       :type :vl-instance-interface-port-bad-connection
       :msg
       "~a0: unsupported interface port argument .~s1(~a2). ~
                         We currently only support arguments with modport ~
                         specifiers for direct interface instantiations, but ~
                         modport ~s3 is found via ~a4."
       :args (list inst port.name
                   expr step1.item.name step2.item))
      arg))
    ((vl-modinst step2.item))
    (iface (vl-scopestack-find-definition step2.item.modname ss))
    ((unless (and iface (vl-scopedef-interface-p iface)))
     (mv
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: unsupported interface port argument .~s1(~a2). ~
                         Expected the modport ~s3 to be inside an interface, ~
                         but found it inside ~s4 which is a ~a5.  Thought ~
                         that modports should only occur in interfaces."
       :args (list inst port.name
                   expr step1.item.name step2.name iface))
      arg))
    ((vl-interface iface))
    ((unless (equal iface.name port.ifname))
     (mv
      (fatal
       :type :vl-instance-interface-port-bad-connection
       :msg
       "~a0: type error: interface port ~s1 (type ~s2) is ~
                         connected to ~a3 (type ~s4)."
       :args (list inst
                   port.name port.ifname expr iface.name))
      arg))
    ((unless (or (not port.modport)
                 (equal port.modport step1.item.name)))
     (mv
      (fatal
       :type :vl-instance-interface-port-bad-connection
       :msg
       "~a0: modport clash for .~s1(~a2).  In submodule ~s3 ~
                         the port is declared as modport ~s4, so you can't ~
                         instantiate it with modport ~s5."
       :args (list inst port.name expr inst.modname
                   port.modport step1.item.name))
      arg))
    ((mv chop-okp
         new-scopeexpr indices ?lastname)
     (vl-scopeexpr-split-right expr.scope))
    ((unless chop-okp)
     (mv
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: reducing interface port .~s1(~a2) by dropping ~
                         modport ~s3: somehow failed to split the modport?"
       :args (list inst port.name expr step1.item.name))
      arg))
    ((when indices)
     (mv
      (fatal
       :type :vl-instance-interface-port-unsupported
       :msg
       "~a0: reducing interface port .~s1(~a2) by dropping ~
                         modport ~s3: indices on pre-modport expression?  ~
                         BOZO we might need to support this for interface ~
                         arrays.")
      arg))
    (modportname-as-expr
     (make-vl-literal :val (make-vl-string :value step1.item.name)))
    (interfacename-as-expr
         (make-vl-literal :val (make-vl-string :value port.ifname)))
    (new-atts (list* (cons "VL_REMOVED_EXPLICIT_MODPORT"
                           modportname-as-expr)
                     (cons "VL_INTERFACE_NAME"
                           interfacename-as-expr)
                     arg.atts))
    (new-arg (change-vl-plainarg
                  arg
                  :expr (change-vl-index expr
                                         :scope new-scopeexpr)
                  :atts new-atts)))
   (mv (ok) new-arg))))

Theorem: vl-warninglist-p-of-vl-unhierarchicalize-interfaceport.warnings

(defthm
    vl-warninglist-p-of-vl-unhierarchicalize-interfaceport.warnings
 (b*
  (((mv ?warnings ?new-arg)
    (vl-unhierarchicalize-interfaceport arg port ss inst warnings)))
  (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-plainarg-p-of-vl-unhierarchicalize-interfaceport.new-arg

(defthm vl-plainarg-p-of-vl-unhierarchicalize-interfaceport.new-arg
 (b*
  (((mv ?warnings ?new-arg)
    (vl-unhierarchicalize-interfaceport arg port ss inst warnings)))
  (vl-plainarg-p new-arg))
 :rule-classes :rewrite)

Theorem: vl-unhierarchicalize-interfaceport-of-vl-plainarg-fix-arg

(defthm vl-unhierarchicalize-interfaceport-of-vl-plainarg-fix-arg
 (equal
    (vl-unhierarchicalize-interfaceport (vl-plainarg-fix arg)
                                        port ss inst warnings)
    (vl-unhierarchicalize-interfaceport arg port ss inst warnings)))

Theorem: vl-unhierarchicalize-interfaceport-vl-plainarg-equiv-congruence-on-arg

(defthm
 vl-unhierarchicalize-interfaceport-vl-plainarg-equiv-congruence-on-arg
 (implies
  (vl-plainarg-equiv arg arg-equiv)
  (equal
      (vl-unhierarchicalize-interfaceport arg port ss inst warnings)
      (vl-unhierarchicalize-interfaceport
           arg-equiv port ss inst warnings)))
 :rule-classes :congruence)

Theorem: vl-unhierarchicalize-interfaceport-of-vl-port-fix-port

(defthm vl-unhierarchicalize-interfaceport-of-vl-port-fix-port
 (equal
    (vl-unhierarchicalize-interfaceport arg (vl-port-fix port)
                                        ss inst warnings)
    (vl-unhierarchicalize-interfaceport arg port ss inst warnings)))

Theorem: vl-unhierarchicalize-interfaceport-vl-port-equiv-congruence-on-port

(defthm
 vl-unhierarchicalize-interfaceport-vl-port-equiv-congruence-on-port
 (implies
  (vl-port-equiv port port-equiv)
  (equal
      (vl-unhierarchicalize-interfaceport arg port ss inst warnings)
      (vl-unhierarchicalize-interfaceport
           arg port-equiv ss inst warnings)))
 :rule-classes :congruence)

Theorem: vl-unhierarchicalize-interfaceport-of-vl-scopestack-fix-ss

(defthm vl-unhierarchicalize-interfaceport-of-vl-scopestack-fix-ss
 (equal
    (vl-unhierarchicalize-interfaceport
         arg port (vl-scopestack-fix ss)
         inst warnings)
    (vl-unhierarchicalize-interfaceport arg port ss inst warnings)))

Theorem: vl-unhierarchicalize-interfaceport-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-unhierarchicalize-interfaceport-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
      (vl-unhierarchicalize-interfaceport arg port ss inst warnings)
      (vl-unhierarchicalize-interfaceport
           arg port ss-equiv inst warnings)))
 :rule-classes :congruence)

Theorem: vl-unhierarchicalize-interfaceport-of-vl-modinst-fix-inst

(defthm vl-unhierarchicalize-interfaceport-of-vl-modinst-fix-inst
 (equal
    (vl-unhierarchicalize-interfaceport
         arg port ss (vl-modinst-fix inst)
         warnings)
    (vl-unhierarchicalize-interfaceport arg port ss inst warnings)))

Theorem: vl-unhierarchicalize-interfaceport-vl-modinst-equiv-congruence-on-inst

(defthm
 vl-unhierarchicalize-interfaceport-vl-modinst-equiv-congruence-on-inst
 (implies
  (vl-modinst-equiv inst inst-equiv)
  (equal
      (vl-unhierarchicalize-interfaceport arg port ss inst warnings)
      (vl-unhierarchicalize-interfaceport
           arg port ss inst-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-unhierarchicalize-interfaceport-of-vl-warninglist-fix-warnings

(defthm
  vl-unhierarchicalize-interfaceport-of-vl-warninglist-fix-warnings
 (equal
    (vl-unhierarchicalize-interfaceport
         arg port
         ss inst (vl-warninglist-fix warnings))
    (vl-unhierarchicalize-interfaceport arg port ss inst warnings)))

Theorem: vl-unhierarchicalize-interfaceport-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-unhierarchicalize-interfaceport-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
      (vl-unhierarchicalize-interfaceport arg port ss inst warnings)
      (vl-unhierarchicalize-interfaceport
           arg port ss inst warnings-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-hidexpr-split-right

Split off the rightmost part of a hierarchical identifier.

Vl-scopeexpr-split-right

Split off the rightmost part of a hierarchical scope expression.