• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
          • Vl-vardecllist-mockmembers
          • Vl-vardecl-mockmember
          • Vl-interfacename-mocktype
          • Vl-modinst-interface-mockmember
          • Vl-interfaceport-mockmember
          • Vl-generate-interface-mockmember
          • Vl-genblock-interface-mockmember
          • Vl-genblob-interface-mocktype
          • Vl-modinstlist-interface-mockmembers
          • Vl-interfaceportlist-mockmembers
          • Vl-generatelist-interface-mockmembers
          • Vl-genblocklist-interface-mockmembers
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Hierarchy
        • Extract-vl-types
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Mlib

Vl-interface-mocktype

Create a datatype that corresponds to an already-elaborated interface.

Signature

(vl-interface-mocktype x ss &key (reclimit '1000)) 
  → 
(mv err type)

Arguments

x — Guard (vl-interface-p x).

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

reclimit — Guard (natp reclimit).

Returns

err — Type (iff (vl-msg-p err) err).

type — Type (and (vl-datatype-p type) (not (vl-datatype->udims type))).

In many ways interface instances are like ordinary variables: they can be passed to submodules, arrays of them can be indexed into, etc. In our SV conversion we want to represent the data associated with an interface instance in the same way as if it were just a structure.

This is tricky because an interface is not actually a datatype, so we can't just reuse convenient (and complicated) functions like vl-datatype-size on them. Rather than duplicate the code, we make a ``mock'' datatype that corresponds to the data portion of an interface.

Theorem: return-type-of-vl-interface-mocktype.err

(defthm return-type-of-vl-interface-mocktype.err
        (b* (((mv ?err common-lisp::?type)
              (vl-interface-mocktype-fn x ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-interface-mocktype.type

(defthm return-type-of-vl-interface-mocktype.type
        (b* (((mv ?err common-lisp::?type)
              (vl-interface-mocktype-fn x ss reclimit)))
            (and (vl-datatype-p type)
                 (not (vl-datatype->udims type))))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-genblob-interface-mocktype.err

(defthm return-type-of-vl-genblob-interface-mocktype.err
        (b* (((mv ?err common-lisp::?type)
              (vl-genblob-interface-mocktype-fn x ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-genblob-interface-mocktype.type

(defthm return-type-of-vl-genblob-interface-mocktype.type
        (b* (((mv ?err common-lisp::?type)
              (vl-genblob-interface-mocktype-fn x ss reclimit)))
            (and (vl-datatype-p type)
                 (not (vl-datatype->udims type))))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-interfacename-mocktype.err

(defthm return-type-of-vl-interfacename-mocktype.err
        (b* (((mv ?err common-lisp::?type)
              (vl-interfacename-mocktype-fn name ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-interfacename-mocktype.type

(defthm return-type-of-vl-interfacename-mocktype.type
        (b* (((mv ?err common-lisp::?type)
              (vl-interfacename-mocktype-fn name ss reclimit)))
            (and (iff (vl-datatype-p type) type)
                 (implies type (not (vl-datatype->udims type)))
                 (implies (not err) type)))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-modinst-interface-mockmember.err

(defthm return-type-of-vl-modinst-interface-mockmember.err
        (b* (((mv ?err common-lisp::?member)
              (vl-modinst-interface-mockmember-fn x ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-modinst-interface-mockmember.member

(defthm return-type-of-vl-modinst-interface-mockmember.member
        (b* (((mv ?err common-lisp::?member)
              (vl-modinst-interface-mockmember-fn x ss reclimit)))
            (and (iff (vl-structmember-p member) member)
                 (implies (not err) member)))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-modinstlist-interface-mockmembers.err

(defthm
     return-type-of-vl-modinstlist-interface-mockmembers.err
     (b* (((mv ?err ?members)
           (vl-modinstlist-interface-mockmembers-fn x ss reclimit)))
         (iff (vl-msg-p err) err))
     :rule-classes :rewrite)

Theorem: return-type-of-vl-modinstlist-interface-mockmembers.members

(defthm
     return-type-of-vl-modinstlist-interface-mockmembers.members
     (b* (((mv ?err ?members)
           (vl-modinstlist-interface-mockmembers-fn x ss reclimit)))
         (vl-structmemberlist-p members))
     :rule-classes :rewrite)

Theorem: return-type-of-vl-interfaceport-mockmember.err

(defthm return-type-of-vl-interfaceport-mockmember.err
        (b* (((mv ?err common-lisp::?member)
              (vl-interfaceport-mockmember-fn x ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-interfaceport-mockmember.member

(defthm return-type-of-vl-interfaceport-mockmember.member
        (b* (((mv ?err common-lisp::?member)
              (vl-interfaceport-mockmember-fn x ss reclimit)))
            (and (iff (vl-structmember-p member) member)
                 (implies (not err) member)))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-interfaceportlist-mockmembers.err

(defthm return-type-of-vl-interfaceportlist-mockmembers.err
        (b* (((mv ?err ?members)
              (vl-interfaceportlist-mockmembers-fn x ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-interfaceportlist-mockmembers.members

(defthm return-type-of-vl-interfaceportlist-mockmembers.members
        (b* (((mv ?err ?members)
              (vl-interfaceportlist-mockmembers-fn x ss reclimit)))
            (vl-structmemberlist-p members))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-generate-interface-mockmember.err

(defthm return-type-of-vl-generate-interface-mockmember.err
        (b* (((mv ?err common-lisp::?member)
              (vl-generate-interface-mockmember-fn x ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-generate-interface-mockmember.member

(defthm return-type-of-vl-generate-interface-mockmember.member
        (b* (((mv ?err common-lisp::?member)
              (vl-generate-interface-mockmember-fn x ss reclimit)))
            (and (iff (vl-structmember-p member) member)
                 (implies (not err) member)))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-generatelist-interface-mockmembers.err

(defthm
    return-type-of-vl-generatelist-interface-mockmembers.err
    (b* (((mv ?err ?members)
          (vl-generatelist-interface-mockmembers-fn x ss reclimit)))
        (iff (vl-msg-p err) err))
    :rule-classes :rewrite)

Theorem: return-type-of-vl-generatelist-interface-mockmembers.members

(defthm
    return-type-of-vl-generatelist-interface-mockmembers.members
    (b* (((mv ?err ?members)
          (vl-generatelist-interface-mockmembers-fn x ss reclimit)))
        (vl-structmemberlist-p members))
    :rule-classes :rewrite)

Theorem: return-type-of-vl-genblock-interface-mockmember.err

(defthm return-type-of-vl-genblock-interface-mockmember.err
        (b* (((mv ?err common-lisp::?member)
              (vl-genblock-interface-mockmember-fn x ss reclimit)))
            (iff (vl-msg-p err) err))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-genblock-interface-mockmember.member

(defthm return-type-of-vl-genblock-interface-mockmember.member
        (b* (((mv ?err common-lisp::?member)
              (vl-genblock-interface-mockmember-fn x ss reclimit)))
            (and (iff (vl-structmember-p member) member)
                 (implies (not err) member)))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-genblocklist-interface-mockmembers.err

(defthm
    return-type-of-vl-genblocklist-interface-mockmembers.err
    (b* (((mv ?err ?members)
          (vl-genblocklist-interface-mockmembers-fn x ss reclimit)))
        (iff (vl-msg-p err) err))
    :rule-classes :rewrite)

Theorem: return-type-of-vl-genblocklist-interface-mockmembers.members

(defthm
    return-type-of-vl-genblocklist-interface-mockmembers.members
    (b* (((mv ?err ?members)
          (vl-genblocklist-interface-mockmembers-fn x ss reclimit)))
        (vl-structmemberlist-p members))
    :rule-classes :rewrite)

Theorem: vl-interface-mocktype-fn-of-vl-interface-fix-x

(defthm vl-interface-mocktype-fn-of-vl-interface-fix-x
        (equal (vl-interface-mocktype-fn (vl-interface-fix x)
                                         ss reclimit)
               (vl-interface-mocktype-fn x ss reclimit)))

Theorem: vl-interface-mocktype-fn-of-vl-scopestack-fix-ss

(defthm vl-interface-mocktype-fn-of-vl-scopestack-fix-ss
        (equal (vl-interface-mocktype-fn x (vl-scopestack-fix ss)
                                         reclimit)
               (vl-interface-mocktype-fn x ss reclimit)))

Theorem: vl-interface-mocktype-fn-of-nfix-reclimit

(defthm vl-interface-mocktype-fn-of-nfix-reclimit
        (equal (vl-interface-mocktype-fn x ss (nfix reclimit))
               (vl-interface-mocktype-fn x ss reclimit)))

Theorem: vl-genblob-interface-mocktype-fn-of-vl-genblob-fix-x

(defthm vl-genblob-interface-mocktype-fn-of-vl-genblob-fix-x
        (equal (vl-genblob-interface-mocktype-fn (vl-genblob-fix x)
                                                 ss reclimit)
               (vl-genblob-interface-mocktype-fn x ss reclimit)))

Theorem: vl-genblob-interface-mocktype-fn-of-vl-scopestack-fix-ss

(defthm
   vl-genblob-interface-mocktype-fn-of-vl-scopestack-fix-ss
   (equal (vl-genblob-interface-mocktype-fn x (vl-scopestack-fix ss)
                                            reclimit)
          (vl-genblob-interface-mocktype-fn x ss reclimit)))

Theorem: vl-genblob-interface-mocktype-fn-of-nfix-reclimit

(defthm
     vl-genblob-interface-mocktype-fn-of-nfix-reclimit
     (equal (vl-genblob-interface-mocktype-fn x ss (nfix reclimit))
            (vl-genblob-interface-mocktype-fn x ss reclimit)))

Theorem: vl-interfacename-mocktype-fn-of-str-fix-name

(defthm vl-interfacename-mocktype-fn-of-str-fix-name
        (equal (vl-interfacename-mocktype-fn (str-fix name)
                                             ss reclimit)
               (vl-interfacename-mocktype-fn name ss reclimit)))

Theorem: vl-interfacename-mocktype-fn-of-vl-scopestack-fix-ss

(defthm
    vl-interfacename-mocktype-fn-of-vl-scopestack-fix-ss
    (equal (vl-interfacename-mocktype-fn name (vl-scopestack-fix ss)
                                         reclimit)
           (vl-interfacename-mocktype-fn name ss reclimit)))

Theorem: vl-interfacename-mocktype-fn-of-nfix-reclimit

(defthm
     vl-interfacename-mocktype-fn-of-nfix-reclimit
     (equal (vl-interfacename-mocktype-fn name ss (nfix reclimit))
            (vl-interfacename-mocktype-fn name ss reclimit)))

Theorem: vl-modinst-interface-mockmember-fn-of-vl-modinst-fix-x

(defthm
     vl-modinst-interface-mockmember-fn-of-vl-modinst-fix-x
     (equal (vl-modinst-interface-mockmember-fn (vl-modinst-fix x)
                                                ss reclimit)
            (vl-modinst-interface-mockmember-fn x ss reclimit)))

Theorem: vl-modinst-interface-mockmember-fn-of-vl-scopestack-fix-ss

(defthm
 vl-modinst-interface-mockmember-fn-of-vl-scopestack-fix-ss
 (equal (vl-modinst-interface-mockmember-fn x (vl-scopestack-fix ss)
                                            reclimit)
        (vl-modinst-interface-mockmember-fn x ss reclimit)))

Theorem: vl-modinst-interface-mockmember-fn-of-nfix-reclimit

(defthm
    vl-modinst-interface-mockmember-fn-of-nfix-reclimit
    (equal (vl-modinst-interface-mockmember-fn x ss (nfix reclimit))
           (vl-modinst-interface-mockmember-fn x ss reclimit)))

Theorem: vl-modinstlist-interface-mockmembers-fn-of-vl-modinstlist-fix-x

(defthm
 vl-modinstlist-interface-mockmembers-fn-of-vl-modinstlist-fix-x
 (equal
     (vl-modinstlist-interface-mockmembers-fn (vl-modinstlist-fix x)
                                              ss reclimit)
     (vl-modinstlist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-modinstlist-interface-mockmembers-fn-of-vl-scopestack-fix-ss

(defthm
 vl-modinstlist-interface-mockmembers-fn-of-vl-scopestack-fix-ss
 (equal
   (vl-modinstlist-interface-mockmembers-fn x (vl-scopestack-fix ss)
                                            reclimit)
   (vl-modinstlist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-modinstlist-interface-mockmembers-fn-of-nfix-reclimit

(defthm
 vl-modinstlist-interface-mockmembers-fn-of-nfix-reclimit
 (equal
      (vl-modinstlist-interface-mockmembers-fn x ss (nfix reclimit))
      (vl-modinstlist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-interfaceport-mockmember-fn-of-vl-interfaceport-fix-x

(defthm
     vl-interfaceport-mockmember-fn-of-vl-interfaceport-fix-x
     (equal (vl-interfaceport-mockmember-fn (vl-interfaceport-fix x)
                                            ss reclimit)
            (vl-interfaceport-mockmember-fn x ss reclimit)))

Theorem: vl-interfaceport-mockmember-fn-of-vl-scopestack-fix-ss

(defthm
     vl-interfaceport-mockmember-fn-of-vl-scopestack-fix-ss
     (equal (vl-interfaceport-mockmember-fn x (vl-scopestack-fix ss)
                                            reclimit)
            (vl-interfaceport-mockmember-fn x ss reclimit)))

Theorem: vl-interfaceport-mockmember-fn-of-nfix-reclimit

(defthm vl-interfaceport-mockmember-fn-of-nfix-reclimit
        (equal (vl-interfaceport-mockmember-fn x ss (nfix reclimit))
               (vl-interfaceport-mockmember-fn x ss reclimit)))

Theorem: vl-interfaceportlist-mockmembers-fn-of-vl-interfaceportlist-fix-x

(defthm
 vl-interfaceportlist-mockmembers-fn-of-vl-interfaceportlist-fix-x
 (equal
   (vl-interfaceportlist-mockmembers-fn (vl-interfaceportlist-fix x)
                                        ss reclimit)
   (vl-interfaceportlist-mockmembers-fn x ss reclimit)))

Theorem: vl-interfaceportlist-mockmembers-fn-of-vl-scopestack-fix-ss

(defthm
  vl-interfaceportlist-mockmembers-fn-of-vl-scopestack-fix-ss
  (equal
       (vl-interfaceportlist-mockmembers-fn x (vl-scopestack-fix ss)
                                            reclimit)
       (vl-interfaceportlist-mockmembers-fn x ss reclimit)))

Theorem: vl-interfaceportlist-mockmembers-fn-of-nfix-reclimit

(defthm
   vl-interfaceportlist-mockmembers-fn-of-nfix-reclimit
   (equal (vl-interfaceportlist-mockmembers-fn x ss (nfix reclimit))
          (vl-interfaceportlist-mockmembers-fn x ss reclimit)))

Theorem: vl-generate-interface-mockmember-fn-of-vl-genelement-fix-x

(defthm
   vl-generate-interface-mockmember-fn-of-vl-genelement-fix-x
   (equal (vl-generate-interface-mockmember-fn (vl-genelement-fix x)
                                               ss reclimit)
          (vl-generate-interface-mockmember-fn x ss reclimit)))

Theorem: vl-generate-interface-mockmember-fn-of-vl-scopestack-fix-ss

(defthm
  vl-generate-interface-mockmember-fn-of-vl-scopestack-fix-ss
  (equal
       (vl-generate-interface-mockmember-fn x (vl-scopestack-fix ss)
                                            reclimit)
       (vl-generate-interface-mockmember-fn x ss reclimit)))

Theorem: vl-generate-interface-mockmember-fn-of-nfix-reclimit

(defthm
   vl-generate-interface-mockmember-fn-of-nfix-reclimit
   (equal (vl-generate-interface-mockmember-fn x ss (nfix reclimit))
          (vl-generate-interface-mockmember-fn x ss reclimit)))

Theorem: vl-generatelist-interface-mockmembers-fn-of-vl-genelementlist-fix-x

(defthm
 vl-generatelist-interface-mockmembers-fn-of-vl-genelementlist-fix-x
 (equal (vl-generatelist-interface-mockmembers-fn
             (vl-genelementlist-fix x)
             ss reclimit)
        (vl-generatelist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-generatelist-interface-mockmembers-fn-of-vl-scopestack-fix-ss

(defthm
 vl-generatelist-interface-mockmembers-fn-of-vl-scopestack-fix-ss
 (equal
  (vl-generatelist-interface-mockmembers-fn x (vl-scopestack-fix ss)
                                            reclimit)
  (vl-generatelist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-generatelist-interface-mockmembers-fn-of-nfix-reclimit

(defthm
 vl-generatelist-interface-mockmembers-fn-of-nfix-reclimit
 (equal
     (vl-generatelist-interface-mockmembers-fn x ss (nfix reclimit))
     (vl-generatelist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-genblock-interface-mockmember-fn-of-vl-genblock-fix-x

(defthm
     vl-genblock-interface-mockmember-fn-of-vl-genblock-fix-x
     (equal (vl-genblock-interface-mockmember-fn (vl-genblock-fix x)
                                                 ss reclimit)
            (vl-genblock-interface-mockmember-fn x ss reclimit)))

Theorem: vl-genblock-interface-mockmember-fn-of-vl-scopestack-fix-ss

(defthm
  vl-genblock-interface-mockmember-fn-of-vl-scopestack-fix-ss
  (equal
       (vl-genblock-interface-mockmember-fn x (vl-scopestack-fix ss)
                                            reclimit)
       (vl-genblock-interface-mockmember-fn x ss reclimit)))

Theorem: vl-genblock-interface-mockmember-fn-of-nfix-reclimit

(defthm
   vl-genblock-interface-mockmember-fn-of-nfix-reclimit
   (equal (vl-genblock-interface-mockmember-fn x ss (nfix reclimit))
          (vl-genblock-interface-mockmember-fn x ss reclimit)))

Theorem: vl-genblocklist-interface-mockmembers-fn-of-vl-genblocklist-fix-x

(defthm
 vl-genblocklist-interface-mockmembers-fn-of-vl-genblocklist-fix-x
 (equal
   (vl-genblocklist-interface-mockmembers-fn (vl-genblocklist-fix x)
                                             ss reclimit)
   (vl-genblocklist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-genblocklist-interface-mockmembers-fn-of-vl-scopestack-fix-ss

(defthm
 vl-genblocklist-interface-mockmembers-fn-of-vl-scopestack-fix-ss
 (equal
  (vl-genblocklist-interface-mockmembers-fn x (vl-scopestack-fix ss)
                                            reclimit)
  (vl-genblocklist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-genblocklist-interface-mockmembers-fn-of-nfix-reclimit

(defthm
 vl-genblocklist-interface-mockmembers-fn-of-nfix-reclimit
 (equal
     (vl-genblocklist-interface-mockmembers-fn x ss (nfix reclimit))
     (vl-genblocklist-interface-mockmembers-fn x ss reclimit)))

Theorem: vl-interface-mocktype-fn-vl-interface-equiv-congruence-on-x

(defthm
    vl-interface-mocktype-fn-vl-interface-equiv-congruence-on-x
    (implies (vl-interface-equiv x x-equiv)
             (equal (vl-interface-mocktype-fn x ss reclimit)
                    (vl-interface-mocktype-fn x-equiv ss reclimit)))
    :rule-classes :congruence)

Theorem: vl-interface-mocktype-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
    vl-interface-mocktype-fn-vl-scopestack-equiv-congruence-on-ss
    (implies (vl-scopestack-equiv ss ss-equiv)
             (equal (vl-interface-mocktype-fn x ss reclimit)
                    (vl-interface-mocktype-fn x ss-equiv reclimit)))
    :rule-classes :congruence)

Theorem: vl-interface-mocktype-fn-nat-equiv-congruence-on-reclimit

(defthm
    vl-interface-mocktype-fn-nat-equiv-congruence-on-reclimit
    (implies (acl2::nat-equiv reclimit reclimit-equiv)
             (equal (vl-interface-mocktype-fn x ss reclimit)
                    (vl-interface-mocktype-fn x ss reclimit-equiv)))
    :rule-classes :congruence)

Theorem: vl-genblob-interface-mocktype-fn-vl-genblob-equiv-congruence-on-x

(defthm
 vl-genblob-interface-mocktype-fn-vl-genblob-equiv-congruence-on-x
 (implies
     (vl-genblob-equiv x x-equiv)
     (equal (vl-genblob-interface-mocktype-fn x ss reclimit)
            (vl-genblob-interface-mocktype-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-genblob-interface-mocktype-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-genblob-interface-mocktype-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
     (vl-scopestack-equiv ss ss-equiv)
     (equal (vl-genblob-interface-mocktype-fn x ss reclimit)
            (vl-genblob-interface-mocktype-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-genblob-interface-mocktype-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-genblob-interface-mocktype-fn-nat-equiv-congruence-on-reclimit
 (implies
     (acl2::nat-equiv reclimit reclimit-equiv)
     (equal (vl-genblob-interface-mocktype-fn x ss reclimit)
            (vl-genblob-interface-mocktype-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-interfacename-mocktype-fn-streqv-congruence-on-name

(defthm
 vl-interfacename-mocktype-fn-streqv-congruence-on-name
 (implies
      (streqv name name-equiv)
      (equal (vl-interfacename-mocktype-fn name ss reclimit)
             (vl-interfacename-mocktype-fn name-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-interfacename-mocktype-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-interfacename-mocktype-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
      (vl-scopestack-equiv ss ss-equiv)
      (equal (vl-interfacename-mocktype-fn name ss reclimit)
             (vl-interfacename-mocktype-fn name ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-interfacename-mocktype-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-interfacename-mocktype-fn-nat-equiv-congruence-on-reclimit
 (implies
      (acl2::nat-equiv reclimit reclimit-equiv)
      (equal (vl-interfacename-mocktype-fn name ss reclimit)
             (vl-interfacename-mocktype-fn name ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-modinst-interface-mockmember-fn-vl-modinst-equiv-congruence-on-x

(defthm
 vl-modinst-interface-mockmember-fn-vl-modinst-equiv-congruence-on-x
 (implies
   (vl-modinst-equiv x x-equiv)
   (equal (vl-modinst-interface-mockmember-fn x ss reclimit)
          (vl-modinst-interface-mockmember-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-modinst-interface-mockmember-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-modinst-interface-mockmember-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal (vl-modinst-interface-mockmember-fn x ss reclimit)
          (vl-modinst-interface-mockmember-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-modinst-interface-mockmember-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-modinst-interface-mockmember-fn-nat-equiv-congruence-on-reclimit
 (implies
   (acl2::nat-equiv reclimit reclimit-equiv)
   (equal (vl-modinst-interface-mockmember-fn x ss reclimit)
          (vl-modinst-interface-mockmember-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-modinstlist-interface-mockmembers-fn-vl-modinstlist-equiv-congruence-on-x

(defthm
 vl-modinstlist-interface-mockmembers-fn-vl-modinstlist-equiv-congruence-on-x
 (implies
  (vl-modinstlist-equiv x x-equiv)
  (equal
     (vl-modinstlist-interface-mockmembers-fn x ss reclimit)
     (vl-modinstlist-interface-mockmembers-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-modinstlist-interface-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-modinstlist-interface-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
     (vl-modinstlist-interface-mockmembers-fn x ss reclimit)
     (vl-modinstlist-interface-mockmembers-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-modinstlist-interface-mockmembers-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-modinstlist-interface-mockmembers-fn-nat-equiv-congruence-on-reclimit
 (implies
  (acl2::nat-equiv reclimit reclimit-equiv)
  (equal
     (vl-modinstlist-interface-mockmembers-fn x ss reclimit)
     (vl-modinstlist-interface-mockmembers-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-interfaceport-mockmember-fn-vl-interfaceport-equiv-congruence-on-x

(defthm
 vl-interfaceport-mockmember-fn-vl-interfaceport-equiv-congruence-on-x
 (implies
      (vl-interfaceport-equiv x x-equiv)
      (equal (vl-interfaceport-mockmember-fn x ss reclimit)
             (vl-interfaceport-mockmember-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-interfaceport-mockmember-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-interfaceport-mockmember-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
      (vl-scopestack-equiv ss ss-equiv)
      (equal (vl-interfaceport-mockmember-fn x ss reclimit)
             (vl-interfaceport-mockmember-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-interfaceport-mockmember-fn-nat-equiv-congruence-on-reclimit

(defthm
  vl-interfaceport-mockmember-fn-nat-equiv-congruence-on-reclimit
  (implies
       (acl2::nat-equiv reclimit reclimit-equiv)
       (equal (vl-interfaceport-mockmember-fn x ss reclimit)
              (vl-interfaceport-mockmember-fn x ss reclimit-equiv)))
  :rule-classes :congruence)

Theorem: vl-interfaceportlist-mockmembers-fn-vl-interfaceportlist-equiv-congruence-on-x

(defthm
 vl-interfaceportlist-mockmembers-fn-vl-interfaceportlist-equiv-congruence-on-x
 (implies
  (vl-interfaceportlist-equiv x x-equiv)
  (equal (vl-interfaceportlist-mockmembers-fn x ss reclimit)
         (vl-interfaceportlist-mockmembers-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-interfaceportlist-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-interfaceportlist-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-interfaceportlist-mockmembers-fn x ss reclimit)
         (vl-interfaceportlist-mockmembers-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-interfaceportlist-mockmembers-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-interfaceportlist-mockmembers-fn-nat-equiv-congruence-on-reclimit
 (implies
  (acl2::nat-equiv reclimit reclimit-equiv)
  (equal (vl-interfaceportlist-mockmembers-fn x ss reclimit)
         (vl-interfaceportlist-mockmembers-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-generate-interface-mockmember-fn-vl-genelement-equiv-congruence-on-x

(defthm
 vl-generate-interface-mockmember-fn-vl-genelement-equiv-congruence-on-x
 (implies
  (vl-genelement-equiv x x-equiv)
  (equal (vl-generate-interface-mockmember-fn x ss reclimit)
         (vl-generate-interface-mockmember-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-generate-interface-mockmember-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-generate-interface-mockmember-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-generate-interface-mockmember-fn x ss reclimit)
         (vl-generate-interface-mockmember-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-generate-interface-mockmember-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-generate-interface-mockmember-fn-nat-equiv-congruence-on-reclimit
 (implies
  (acl2::nat-equiv reclimit reclimit-equiv)
  (equal (vl-generate-interface-mockmember-fn x ss reclimit)
         (vl-generate-interface-mockmember-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-generatelist-interface-mockmembers-fn-vl-genelementlist-equiv-congruence-on-x

(defthm
 vl-generatelist-interface-mockmembers-fn-vl-genelementlist-equiv-congruence-on-x
 (implies
  (vl-genelementlist-equiv x x-equiv)
  (equal
    (vl-generatelist-interface-mockmembers-fn x ss reclimit)
    (vl-generatelist-interface-mockmembers-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-generatelist-interface-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-generatelist-interface-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
    (vl-generatelist-interface-mockmembers-fn x ss reclimit)
    (vl-generatelist-interface-mockmembers-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-generatelist-interface-mockmembers-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-generatelist-interface-mockmembers-fn-nat-equiv-congruence-on-reclimit
 (implies
  (acl2::nat-equiv reclimit reclimit-equiv)
  (equal
    (vl-generatelist-interface-mockmembers-fn x ss reclimit)
    (vl-generatelist-interface-mockmembers-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-genblock-interface-mockmember-fn-vl-genblock-equiv-congruence-on-x

(defthm
 vl-genblock-interface-mockmember-fn-vl-genblock-equiv-congruence-on-x
 (implies
  (vl-genblock-equiv x x-equiv)
  (equal (vl-genblock-interface-mockmember-fn x ss reclimit)
         (vl-genblock-interface-mockmember-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-genblock-interface-mockmember-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-genblock-interface-mockmember-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-genblock-interface-mockmember-fn x ss reclimit)
         (vl-genblock-interface-mockmember-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-genblock-interface-mockmember-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-genblock-interface-mockmember-fn-nat-equiv-congruence-on-reclimit
 (implies
  (acl2::nat-equiv reclimit reclimit-equiv)
  (equal (vl-genblock-interface-mockmember-fn x ss reclimit)
         (vl-genblock-interface-mockmember-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Theorem: vl-genblocklist-interface-mockmembers-fn-vl-genblocklist-equiv-congruence-on-x

(defthm
 vl-genblocklist-interface-mockmembers-fn-vl-genblocklist-equiv-congruence-on-x
 (implies
  (vl-genblocklist-equiv x x-equiv)
  (equal
    (vl-genblocklist-interface-mockmembers-fn x ss reclimit)
    (vl-genblocklist-interface-mockmembers-fn x-equiv ss reclimit)))
 :rule-classes :congruence)

Theorem: vl-genblocklist-interface-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-genblocklist-interface-mockmembers-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
    (vl-genblocklist-interface-mockmembers-fn x ss reclimit)
    (vl-genblocklist-interface-mockmembers-fn x ss-equiv reclimit)))
 :rule-classes :congruence)

Theorem: vl-genblocklist-interface-mockmembers-fn-nat-equiv-congruence-on-reclimit

(defthm
 vl-genblocklist-interface-mockmembers-fn-nat-equiv-congruence-on-reclimit
 (implies
  (acl2::nat-equiv reclimit reclimit-equiv)
  (equal
    (vl-genblocklist-interface-mockmembers-fn x ss reclimit)
    (vl-genblocklist-interface-mockmembers-fn x ss reclimit-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-vardecllist-mockmembers

(vl-vardecllist-mockmembers x) maps vl-vardecl-mockmember across a list.

Vl-vardecl-mockmember

Vl-interfacename-mocktype

Vl-modinst-interface-mockmember

Vl-interfaceport-mockmember

Vl-generate-interface-mockmember

Vl-genblock-interface-mockmember

Vl-genblob-interface-mocktype

Vl-modinstlist-interface-mockmembers

Vl-interfaceportlist-mockmembers

Vl-generatelist-interface-mockmembers

Vl-genblocklist-interface-mockmembers