		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-normalize-ifs

Try to push data IFs down, pull clock IFs up, and align the polarity of clock-based IFs with the edge declarations.

Signature
(vl-edgesynth-normalize-ifs x edgetable) → new-stmt
Arguments: x — Guard (and (vl-stmt-p x) (vl-edgesynth-stmt-p x)).; edgetable — Guard (vl-edgetable-p edgetable).
Returns: new-stmt — Type (vl-edgesynth-stmt-p new-stmt), given the guard.

Definitions and Theorems

Function: vl-edgesynth-normalize-ifs

(defun vl-edgesynth-normalize-ifs (x edgetable)
 (declare (xargs :guard (and (and (vl-stmt-p x)
                                  (vl-edgesynth-stmt-p x))
                             (vl-edgetable-p edgetable))))
 (let ((__function__ 'vl-edgesynth-normalize-ifs))
   (declare (ignorable __function__))
   (b*
    (((when (vl-atomicstmt-p x)) x)
     ((when (vl-ifstmt-p x))
      (b*
       (((vl-ifstmt x) x)
        ((mv type guts)
         (vl-edgesynth-classify-iftest x.condition edgetable))
        (true (vl-edgesynth-normalize-ifs x.truebranch edgetable))
        (false (vl-edgesynth-normalize-ifs x.falsebranch edgetable))
        ((when (eq type :clock))
         (b* ((clockname (vl-idexpr->name guts))
              (edge (cdr (hons-assoc-equal clockname edgetable)))
              (posedgep (vl-edgesynth-edge->posedgep edge))
              ((when posedgep)
               (make-vl-ifstmt :condition guts
                               :truebranch true
                               :falsebranch false)))
           (make-vl-ifstmt :condition (vl-condition-neg guts)
                           :truebranch false
                           :falsebranch true)))
        ((when (eq type :nclock))
         (b* ((clockname (vl-idexpr->name guts))
              (edge (cdr (hons-assoc-equal clockname edgetable)))
              (posedgep (vl-edgesynth-edge->posedgep edge))
              ((when posedgep)
               (make-vl-ifstmt :condition guts
                               :truebranch false
                               :falsebranch true)))
           (make-vl-ifstmt :condition (vl-condition-neg guts)
                           :truebranch true
                           :falsebranch false)))
        ((unless (eq type :data)) x))
       x))
     ((when (vl-blockstmt-p x))
      (raise "Thought we already got rid of block statements!")
      x))
    (raise "Should be impossible.")
    x)))

Theorem: vl-edgesynth-stmt-p-of-vl-edgesynth-normalize-ifs

(defthm vl-edgesynth-stmt-p-of-vl-edgesynth-normalize-ifs
  (implies (and (force (if (vl-stmt-p x)
                           (vl-edgesynth-stmt-p x)
                         'nil))
                (force (vl-edgetable-p edgetable)))
           (b* ((new-stmt (vl-edgesynth-normalize-ifs x edgetable)))
             (vl-edgesynth-stmt-p new-stmt)))
  :rule-classes :rewrite)