• Top
  • Documentation
  • Books
  • 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
        • Extract-vl-types
        • Hierarchy
        • 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
  • Math
  • Testing-utilities

• 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