(vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) → (mv portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)
Function:
(defun vl-sort-genelements-aux (x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (declare (xargs :guard (and (vl-genelementlist-p x) (vl-portdecllist-p portdecls) (vl-assignlist-p assigns) (vl-aliaslist-p aliases) (vl-vardecllist-p vardecls) (vl-paramdecllist-p paramdecls) (vl-fundecllist-p fundecls) (vl-taskdecllist-p taskdecls) (vl-modinstlist-p modinsts) (vl-gateinstlist-p gateinsts) (vl-alwayslist-p alwayses) (vl-initiallist-p initials) (vl-finallist-p finals) (vl-typedeflist-p typedefs) (vl-importlist-p imports) (vl-fwdtypedeflist-p fwdtypedefs) (vl-modportlist-p modports) (vl-genvarlist-p genvars) (vl-assertionlist-p assertions) (vl-cassertionlist-p cassertions) (vl-propertylist-p properties) (vl-sequencelist-p sequences) (vl-clkdecllist-p clkdecls) (vl-gclkdecllist-p gclkdecls) (vl-defaultdisablelist-p defaultdisables) (vl-dpiimportlist-p dpiimports) (vl-dpiexportlist-p dpiexports) (vl-bindlist-p binds) (vl-classlist-p classes) (vl-covergrouplist-p covergroups) (vl-elabtasklist-p elabtasks) (vl-letdecllist-p letdecls) (vl-genelementlist-p generates)))) (let ((__function__ 'vl-sort-genelements-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (rev (vl-portdecllist-fix portdecls)) (rev (vl-assignlist-fix assigns)) (rev (vl-aliaslist-fix aliases)) (rev (vl-vardecllist-fix vardecls)) (rev (vl-paramdecllist-fix paramdecls)) (rev (vl-fundecllist-fix fundecls)) (rev (vl-taskdecllist-fix taskdecls)) (rev (vl-modinstlist-fix modinsts)) (rev (vl-gateinstlist-fix gateinsts)) (rev (vl-alwayslist-fix alwayses)) (rev (vl-initiallist-fix initials)) (rev (vl-finallist-fix finals)) (rev (vl-typedeflist-fix typedefs)) (rev (vl-importlist-fix imports)) (rev (vl-fwdtypedeflist-fix fwdtypedefs)) (rev (vl-modportlist-fix modports)) (rev (vl-genvarlist-fix genvars)) (rev (vl-assertionlist-fix assertions)) (rev (vl-cassertionlist-fix cassertions)) (rev (vl-propertylist-fix properties)) (rev (vl-sequencelist-fix sequences)) (rev (vl-clkdecllist-fix clkdecls)) (rev (vl-gclkdecllist-fix gclkdecls)) (rev (vl-defaultdisablelist-fix defaultdisables)) (rev (vl-dpiimportlist-fix dpiimports)) (rev (vl-dpiexportlist-fix dpiexports)) (rev (vl-bindlist-fix binds)) (rev (vl-classlist-fix classes)) (rev (vl-covergrouplist-fix covergroups)) (rev (vl-elabtasklist-fix elabtasks)) (rev (vl-letdecllist-fix letdecls)) (rev (vl-genelementlist-fix generates)))) (xf (car x))) (vl-genelement-case xf :vl-genbase (b* ((x1 xf.item) (tag (tag x1))) (vl-sort-genelements-aux (cdr x) (if (eq tag :vl-portdecl) (cons x1 portdecls) portdecls) (if (eq tag :vl-assign) (cons x1 assigns) assigns) (if (eq tag :vl-alias) (cons x1 aliases) aliases) (if (eq tag :vl-vardecl) (cons x1 vardecls) vardecls) (if (eq tag :vl-paramdecl) (cons x1 paramdecls) paramdecls) (if (eq tag :vl-fundecl) (cons x1 fundecls) fundecls) (if (eq tag :vl-taskdecl) (cons x1 taskdecls) taskdecls) (if (eq tag :vl-modinst) (cons x1 modinsts) modinsts) (if (eq tag :vl-gateinst) (cons x1 gateinsts) gateinsts) (if (eq tag :vl-always) (cons x1 alwayses) alwayses) (if (eq tag :vl-initial) (cons x1 initials) initials) (if (eq tag :vl-final) (cons x1 finals) finals) (if (eq tag :vl-typedef) (cons x1 typedefs) typedefs) (if (eq tag :vl-import) (cons x1 imports) imports) (if (eq tag :vl-fwdtypedef) (cons x1 fwdtypedefs) fwdtypedefs) (if (eq tag :vl-modport) (cons x1 modports) modports) (if (eq tag :vl-genvar) (cons x1 genvars) genvars) (if (eq tag :vl-assertion) (cons x1 assertions) assertions) (if (eq tag :vl-cassertion) (cons x1 cassertions) cassertions) (if (eq tag :vl-property) (cons x1 properties) properties) (if (eq tag :vl-sequence) (cons x1 sequences) sequences) (if (eq tag :vl-clkdecl) (cons x1 clkdecls) clkdecls) (if (eq tag :vl-gclkdecl) (cons x1 gclkdecls) gclkdecls) (if (eq tag :vl-defaultdisable) (cons x1 defaultdisables) defaultdisables) (if (eq tag :vl-dpiimport) (cons x1 dpiimports) dpiimports) (if (eq tag :vl-dpiexport) (cons x1 dpiexports) dpiexports) (if (eq tag :vl-bind) (cons x1 binds) binds) (if (eq tag :vl-class) (cons x1 classes) classes) (if (eq tag :vl-covergroup) (cons x1 covergroups) covergroups) (if (eq tag :vl-elabtask) (cons x1 elabtasks) elabtasks) (if (eq tag :vl-letdecl) (cons x1 letdecls) letdecls) generates)) :otherwise (vl-sort-genelements-aux (cdr x) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls (cons (vl-genelement-fix (car x)) generates))))))
Theorem:
(defthm vl-portdecllist-p-of-vl-sort-genelements-aux.portdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-portdecllist-p portdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-sort-genelements-aux.assigns (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm vl-aliaslist-p-of-vl-sort-genelements-aux.aliases (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-aliaslist-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-sort-genelements-aux.vardecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-p-of-vl-sort-genelements-aux.paramdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-paramdecllist-p paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-fundecllist-p-of-vl-sort-genelements-aux.fundecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-fundecllist-p fundecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-taskdecllist-p-of-vl-sort-genelements-aux.taskdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-taskdecllist-p taskdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-p-of-vl-sort-genelements-aux.modinsts (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-modinstlist-p modinsts)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-p-of-vl-sort-genelements-aux.gateinsts (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-gateinstlist-p gateinsts)) :rule-classes :rewrite)
Theorem:
(defthm vl-alwayslist-p-of-vl-sort-genelements-aux.alwayses (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-alwayslist-p alwayses)) :rule-classes :rewrite)
Theorem:
(defthm vl-initiallist-p-of-vl-sort-genelements-aux.initials (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-initiallist-p initials)) :rule-classes :rewrite)
Theorem:
(defthm vl-finallist-p-of-vl-sort-genelements-aux.finals (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-finallist-p finals)) :rule-classes :rewrite)
Theorem:
(defthm vl-typedeflist-p-of-vl-sort-genelements-aux.typedefs (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-typedeflist-p typedefs)) :rule-classes :rewrite)
Theorem:
(defthm vl-importlist-p-of-vl-sort-genelements-aux.imports (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-importlist-p imports)) :rule-classes :rewrite)
Theorem:
(defthm vl-fwdtypedeflist-p-of-vl-sort-genelements-aux.fwdtypedefs (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-fwdtypedeflist-p fwdtypedefs)) :rule-classes :rewrite)
Theorem:
(defthm vl-modportlist-p-of-vl-sort-genelements-aux.modports (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-modportlist-p modports)) :rule-classes :rewrite)
Theorem:
(defthm vl-genvarlist-p-of-vl-sort-genelements-aux.genvars (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-genvarlist-p genvars)) :rule-classes :rewrite)
Theorem:
(defthm vl-assertionlist-p-of-vl-sort-genelements-aux.assertions (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-assertionlist-p assertions)) :rule-classes :rewrite)
Theorem:
(defthm vl-cassertionlist-p-of-vl-sort-genelements-aux.cassertions (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-cassertionlist-p cassertions)) :rule-classes :rewrite)
Theorem:
(defthm vl-propertylist-p-of-vl-sort-genelements-aux.properties (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-propertylist-p properties)) :rule-classes :rewrite)
Theorem:
(defthm vl-sequencelist-p-of-vl-sort-genelements-aux.sequences (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-sequencelist-p sequences)) :rule-classes :rewrite)
Theorem:
(defthm vl-clkdecllist-p-of-vl-sort-genelements-aux.clkdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-clkdecllist-p clkdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-gclkdecllist-p-of-vl-sort-genelements-aux.gclkdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-gclkdecllist-p gclkdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-defaultdisablelist-p-of-vl-sort-genelements-aux.defaultdisables (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-defaultdisablelist-p defaultdisables)) :rule-classes :rewrite)
Theorem:
(defthm vl-dpiimportlist-p-of-vl-sort-genelements-aux.dpiimports (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-dpiimportlist-p dpiimports)) :rule-classes :rewrite)
Theorem:
(defthm vl-dpiexportlist-p-of-vl-sort-genelements-aux.dpiexports (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-dpiexportlist-p dpiexports)) :rule-classes :rewrite)
Theorem:
(defthm vl-bindlist-p-of-vl-sort-genelements-aux.binds (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-bindlist-p binds)) :rule-classes :rewrite)
Theorem:
(defthm vl-classlist-p-of-vl-sort-genelements-aux.classes (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-classlist-p classes)) :rule-classes :rewrite)
Theorem:
(defthm vl-covergrouplist-p-of-vl-sort-genelements-aux.covergroups (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-covergrouplist-p covergroups)) :rule-classes :rewrite)
Theorem:
(defthm vl-elabtasklist-p-of-vl-sort-genelements-aux.elabtasks (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-elabtasklist-p elabtasks)) :rule-classes :rewrite)
Theorem:
(defthm vl-letdecllist-p-of-vl-sort-genelements-aux.letdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-letdecllist-p letdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-genelementlist-p-of-vl-sort-genelements-aux.generates (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?finals ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?assertions ?cassertions ?properties ?sequences ?clkdecls ?gclkdecls ?defaultdisables ?dpiimports ?dpiexports ?binds ?classes ?covergroups ?elabtasks ?letdecls ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) (vl-genelementlist-p generates)) :rule-classes :rewrite)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-genelementlist-fix-x (equal (vl-sort-genelements-aux (vl-genelementlist-fix x) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-genelementlist-equiv-congruence-on-x (implies (vl-genelementlist-equiv x x-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x-equiv portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-portdecllist-fix-portdecls (equal (vl-sort-genelements-aux x (vl-portdecllist-fix portdecls) assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-portdecllist-equiv-congruence-on-portdecls (implies (vl-portdecllist-equiv portdecls portdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls-equiv assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-assignlist-fix-assigns (equal (vl-sort-genelements-aux x portdecls (vl-assignlist-fix assigns) aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-assignlist-equiv-congruence-on-assigns (implies (vl-assignlist-equiv assigns assigns-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns-equiv aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-aliaslist-fix-aliases (equal (vl-sort-genelements-aux x portdecls assigns (vl-aliaslist-fix aliases) vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-aliaslist-equiv-congruence-on-aliases (implies (vl-aliaslist-equiv aliases aliases-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases-equiv vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-vardecllist-fix-vardecls (equal (vl-sort-genelements-aux x portdecls assigns aliases (vl-vardecllist-fix vardecls) paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-vardecllist-equiv-congruence-on-vardecls (implies (vl-vardecllist-equiv vardecls vardecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls-equiv paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-paramdecllist-fix-paramdecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls (vl-paramdecllist-fix paramdecls) fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-paramdecllist-equiv-congruence-on-paramdecls (implies (vl-paramdecllist-equiv paramdecls paramdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls-equiv fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-fundecllist-fix-fundecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls (vl-fundecllist-fix fundecls) taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-fundecllist-equiv-congruence-on-fundecls (implies (vl-fundecllist-equiv fundecls fundecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls-equiv taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-taskdecllist-fix-taskdecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls (vl-taskdecllist-fix taskdecls) modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-taskdecllist-equiv-congruence-on-taskdecls (implies (vl-taskdecllist-equiv taskdecls taskdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls-equiv modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-modinstlist-fix-modinsts (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls (vl-modinstlist-fix modinsts) gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-modinstlist-equiv-congruence-on-modinsts (implies (vl-modinstlist-equiv modinsts modinsts-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts-equiv gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-gateinstlist-fix-gateinsts (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts (vl-gateinstlist-fix gateinsts) alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-gateinstlist-equiv-congruence-on-gateinsts (implies (vl-gateinstlist-equiv gateinsts gateinsts-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts-equiv alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-alwayslist-fix-alwayses (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts (vl-alwayslist-fix alwayses) initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-alwayslist-equiv-congruence-on-alwayses (implies (vl-alwayslist-equiv alwayses alwayses-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses-equiv initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-initiallist-fix-initials (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses (vl-initiallist-fix initials) finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-initiallist-equiv-congruence-on-initials (implies (vl-initiallist-equiv initials initials-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials-equiv finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-finallist-fix-finals (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials (vl-finallist-fix finals) typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-finallist-equiv-congruence-on-finals (implies (vl-finallist-equiv finals finals-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals-equiv typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-typedeflist-fix-typedefs (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals (vl-typedeflist-fix typedefs) imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-typedeflist-equiv-congruence-on-typedefs (implies (vl-typedeflist-equiv typedefs typedefs-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs-equiv imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-importlist-fix-imports (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs (vl-importlist-fix imports) fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-importlist-equiv-congruence-on-imports (implies (vl-importlist-equiv imports imports-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports-equiv fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-fwdtypedeflist-fix-fwdtypedefs (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports (vl-fwdtypedeflist-fix fwdtypedefs) modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-fwdtypedeflist-equiv-congruence-on-fwdtypedefs (implies (vl-fwdtypedeflist-equiv fwdtypedefs fwdtypedefs-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs-equiv modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-modportlist-fix-modports (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs (vl-modportlist-fix modports) genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-modportlist-equiv-congruence-on-modports (implies (vl-modportlist-equiv modports modports-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports-equiv genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-genvarlist-fix-genvars (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports (vl-genvarlist-fix genvars) assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-genvarlist-equiv-congruence-on-genvars (implies (vl-genvarlist-equiv genvars genvars-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars-equiv assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-assertionlist-fix-assertions (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars (vl-assertionlist-fix assertions) cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-assertionlist-equiv-congruence-on-assertions (implies (vl-assertionlist-equiv assertions assertions-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions-equiv cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-cassertionlist-fix-cassertions (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions (vl-cassertionlist-fix cassertions) properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-cassertionlist-equiv-congruence-on-cassertions (implies (vl-cassertionlist-equiv cassertions cassertions-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions-equiv properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-propertylist-fix-properties (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions (vl-propertylist-fix properties) sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-propertylist-equiv-congruence-on-properties (implies (vl-propertylist-equiv properties properties-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties-equiv sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-sequencelist-fix-sequences (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties (vl-sequencelist-fix sequences) clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-sequencelist-equiv-congruence-on-sequences (implies (vl-sequencelist-equiv sequences sequences-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences-equiv clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-clkdecllist-fix-clkdecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences (vl-clkdecllist-fix clkdecls) gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-clkdecllist-equiv-congruence-on-clkdecls (implies (vl-clkdecllist-equiv clkdecls clkdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls-equiv gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-gclkdecllist-fix-gclkdecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls (vl-gclkdecllist-fix gclkdecls) defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-gclkdecllist-equiv-congruence-on-gclkdecls (implies (vl-gclkdecllist-equiv gclkdecls gclkdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls-equiv defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-defaultdisablelist-fix-defaultdisables (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls (vl-defaultdisablelist-fix defaultdisables) dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-defaultdisablelist-equiv-congruence-on-defaultdisables (implies (vl-defaultdisablelist-equiv defaultdisables defaultdisables-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables-equiv dpiimports dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-dpiimportlist-fix-dpiimports (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables (vl-dpiimportlist-fix dpiimports) dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-dpiimportlist-equiv-congruence-on-dpiimports (implies (vl-dpiimportlist-equiv dpiimports dpiimports-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports-equiv dpiexports binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-dpiexportlist-fix-dpiexports (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports (vl-dpiexportlist-fix dpiexports) binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-dpiexportlist-equiv-congruence-on-dpiexports (implies (vl-dpiexportlist-equiv dpiexports dpiexports-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports-equiv binds classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-bindlist-fix-binds (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports (vl-bindlist-fix binds) classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-bindlist-equiv-congruence-on-binds (implies (vl-bindlist-equiv binds binds-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds-equiv classes covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-classlist-fix-classes (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds (vl-classlist-fix classes) covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-classlist-equiv-congruence-on-classes (implies (vl-classlist-equiv classes classes-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes-equiv covergroups elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-covergrouplist-fix-covergroups (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes (vl-covergrouplist-fix covergroups) elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-covergrouplist-equiv-congruence-on-covergroups (implies (vl-covergrouplist-equiv covergroups covergroups-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups-equiv elabtasks letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-elabtasklist-fix-elabtasks (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups (vl-elabtasklist-fix elabtasks) letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-elabtasklist-equiv-congruence-on-elabtasks (implies (vl-elabtasklist-equiv elabtasks elabtasks-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks-equiv letdecls generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-letdecllist-fix-letdecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks (vl-letdecllist-fix letdecls) generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-letdecllist-equiv-congruence-on-letdecls (implies (vl-letdecllist-equiv letdecls letdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls-equiv generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-genelementlist-fix-generates (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls (vl-genelementlist-fix generates)) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-genelementlist-equiv-congruence-on-generates (implies (vl-genelementlist-equiv generates generates-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates-equiv))) :rule-classes :congruence)