		Search-engine friendly clone of the ACL2 documentation.

Edgesplit

Vl-edgesplit-make-new-always

Create the new, split up always blocks for a single lvalue.

Signature
(vl-edgesplit-make-new-always lvalue ctrl body atts loc) → new-always
Arguments: lvalue — Name of some lvalue. Should be among the lvalues of the body.
Guard (stringp lvalue).; ctrl — Sensitivity list for the original always block. This will become the sensitivity list for each new always block, too.
Guard (and (vl-delayoreventcontrol-p ctrl) (vl-edge-control-p ctrl)).; body — The body of the always block, simple enough to split.
Guard (and (vl-stmt-p body) (vl-edgesplitstmt-p body)).; atts — Attributes of the original always block, which we'll just repeat in each new always block we create.
Guard (vl-atts-p atts).; loc — Location of the original always block, which we'll repeat in each new always block we create.
Guard (vl-location-p loc).
Returns: new-always — Type (vl-always-p new-always), given the guard.

Definitions and Theorems

Function: vl-edgesplit-make-new-always

(defun vl-edgesplit-make-new-always (lvalue ctrl body atts loc)
 (declare (xargs :guard (and (stringp lvalue)
                             (and (vl-delayoreventcontrol-p ctrl)
                                  (vl-edge-control-p ctrl))
                             (and (vl-stmt-p body)
                                  (vl-edgesplitstmt-p body))
                             (vl-atts-p atts)
                             (vl-location-p loc))))
 (let ((__function__ 'vl-edgesplit-make-new-always))
  (declare (ignorable __function__))
  (b*
   ((new-body (vl-edgesplit-stmt-for-lvalue body lvalue))
    ((when (eq (vl-stmt-kind new-body)
               :vl-nullstmt))
     (raise
      "Programming error.  Something is horribly wrong with always
                block splitting.  It shouldn't be possible to try to split
                off a null always block for ~s0."
      lvalue)
     (make-vl-always :type :vl-always
                     :stmt body
                     :loc loc))
    (new-stmt (make-vl-timingstmt :ctrl ctrl
                                  :body new-body))
    (new-always (make-vl-always :type :vl-always
                                :stmt new-stmt
                                :atts atts
                                :loc loc)))
   new-always)))

Theorem: vl-always-p-of-vl-edgesplit-make-new-always

(defthm vl-always-p-of-vl-edgesplit-make-new-always
 (implies
   (and (force (stringp lvalue))
        (force (if (vl-delayoreventcontrol-p ctrl)
                   (vl-edge-control-p ctrl)
                 'nil))
        (force (if (vl-stmt-p body)
                   (vl-edgesplitstmt-p body)
                 'nil))
        (force (vl-atts-p atts))
        (force (vl-location-p loc)))
   (b*
    ((new-always
          (vl-edgesplit-make-new-always lvalue ctrl body atts loc)))
    (vl-always-p new-always)))
 :rule-classes :rewrite)