		Search-engine friendly clone of the ACL2 documentation.

Edgesplit

Vl-always-edgesplit

Signature
(vl-always-edgesplit x) → new-alwayses
Arguments: x — Guard (vl-always-p x).
Returns: new-alwayses — Type (vl-alwayslist-p new-alwayses), given the guard.

Definitions and Theorems

Function: vl-always-edgesplit

(defun vl-always-edgesplit (x)
  (declare (xargs :guard (vl-always-p x)))
  (let ((__function__ 'vl-always-edgesplit))
    (declare (ignorable __function__))
    (b* (((vl-always x) x)
         ((unless (or (eq x.type :vl-always)
                      (eq x.type :vl-always-ff)))
          (list x))
         ((mv body ctrl ?edges)
          (vl-match-always-at-some-edges x.stmt))
         ((unless (and body (vl-edgesplitstmt-p body)))
          (list x))
         (lvalues (mergesort (vl-edgesplitstmt-lvalues body))))
      (vl-edgesplit-make-new-alwayses
           lvalues ctrl body x.atts x.loc))))

Theorem: vl-alwayslist-p-of-vl-always-edgesplit

(defthm vl-alwayslist-p-of-vl-always-edgesplit
  (implies (and (force (vl-always-p x)))
           (b* ((new-alwayses (vl-always-edgesplit x)))
             (vl-alwayslist-p new-alwayses)))
  :rule-classes :rewrite)