		Search-engine friendly clone of the ACL2 documentation.

Genblob

Vl-sort-genelements

Sort a vl-genelementlist-p to create a vl-genblob.

Signature
(vl-sort-genelements x &key (id 'nil) (scopetype ':vl-anonymous-scope)) → blob
Arguments: x — Guard (vl-genelementlist-p x).; id — Guard (vl-maybe-scopeid-p id).; scopetype — Guard (vl-scopetype-p scopetype).
Returns: blob — Type (vl-genblob-p blob).

Definitions and Theorems

Function: vl-sort-genelements-fn

(defun vl-sort-genelements-fn (x id scopetype)
  (declare (xargs :guard (and (vl-genelementlist-p x)
                              (vl-maybe-scopeid-p id)
                              (vl-scopetype-p scopetype))))
  (let ((__function__ 'vl-sort-genelements))
    (declare (ignorable __function__))
    (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 nil nil nil
               nil nil nil nil nil nil nil nil nil nil
               nil nil nil nil nil nil nil nil nil nil
               nil nil nil nil nil nil nil nil nil)))
      (make-vl-genblob :portdecls portdecls
                       :assigns assigns
                       :aliases aliases
                       :vardecls vardecls
                       :paramdecls paramdecls
                       :fundecls fundecls
                       :taskdecls taskdecls
                       :modinsts modinsts
                       :gateinsts gateinsts
                       :alwayses alwayses
                       :initials initials
                       :finals finals
                       :typedefs typedefs
                       :imports imports
                       :fwdtypedefs fwdtypedefs
                       :modports modports
                       :genvars genvars
                       :assertions assertions
                       :cassertions cassertions
                       :properties properties
                       :sequences sequences
                       :clkdecls clkdecls
                       :gclkdecls gclkdecls
                       :defaultdisables defaultdisables
                       :dpiimports dpiimports
                       :dpiexports dpiexports
                       :binds binds
                       :classes classes
                       :covergroups covergroups
                       :elabtasks elabtasks
                       :letdecls letdecls
                       :generates generates
                       :id id
                       :scopetype scopetype))))

Theorem: vl-genblob-p-of-vl-sort-genelements

(defthm vl-genblob-p-of-vl-sort-genelements
  (b* ((blob (vl-sort-genelements-fn x id scopetype)))
    (vl-genblob-p blob))
  :rule-classes :rewrite)

Theorem: vl-sort-genelements-fn-of-vl-genelementlist-fix-x

(defthm vl-sort-genelements-fn-of-vl-genelementlist-fix-x
  (equal (vl-sort-genelements-fn (vl-genelementlist-fix x)
                                 id scopetype)
         (vl-sort-genelements-fn x id scopetype)))

Theorem: vl-sort-genelements-fn-vl-genelementlist-equiv-congruence-on-x

(defthm
     vl-sort-genelements-fn-vl-genelementlist-equiv-congruence-on-x
  (implies (vl-genelementlist-equiv x x-equiv)
           (equal (vl-sort-genelements-fn x id scopetype)
                  (vl-sort-genelements-fn x-equiv id scopetype)))
  :rule-classes :congruence)

Theorem: vl-sort-genelements-fn-of-vl-maybe-scopeid-fix-id

(defthm vl-sort-genelements-fn-of-vl-maybe-scopeid-fix-id
  (equal (vl-sort-genelements-fn x (vl-maybe-scopeid-fix id)
                                 scopetype)
         (vl-sort-genelements-fn x id scopetype)))

Theorem: vl-sort-genelements-fn-vl-maybe-scopeid-equiv-congruence-on-id

(defthm
     vl-sort-genelements-fn-vl-maybe-scopeid-equiv-congruence-on-id
  (implies (vl-maybe-scopeid-equiv id id-equiv)
           (equal (vl-sort-genelements-fn x id scopetype)
                  (vl-sort-genelements-fn x id-equiv scopetype)))
  :rule-classes :congruence)

Theorem: vl-sort-genelements-fn-of-vl-scopetype-fix-scopetype

(defthm vl-sort-genelements-fn-of-vl-scopetype-fix-scopetype
  (equal (vl-sort-genelements-fn x id (vl-scopetype-fix scopetype))
         (vl-sort-genelements-fn x id scopetype)))

Theorem: vl-sort-genelements-fn-vl-scopetype-equiv-congruence-on-scopetype

(defthm
  vl-sort-genelements-fn-vl-scopetype-equiv-congruence-on-scopetype
  (implies (vl-scopetype-equiv scopetype scopetype-equiv)
           (equal (vl-sort-genelements-fn x id scopetype)
                  (vl-sort-genelements-fn x id scopetype-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-sort-genelements-aux