		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-merge-data-ifs

Safely merge if (condition) q <= d1 else q <= d2 into q <= condition ? d1 : d2.

Signature
(vl-edgesynth-merge-data-ifs condition true-branch false-branch nf vardecls assigns) → (mv new-stmt nf vardecls assigns)
Arguments: condition — Should be a data condition.
Guard (vl-expr-p condition).; true-branch — Should be q <= d1 or a null statement.
Guard (and (vl-stmt-p true-branch) (vl-atomicstmt-p true-branch) (vl-edgesynth-stmt-p true-branch)) .; false-branch — Should be q <= d2 or a null statement.
Guard (and (vl-stmt-p false-branch) (vl-atomicstmt-p false-branch) (vl-edgesynth-stmt-p false-branch)) .; nf — Guard (vl-namefactory-p nf).; vardecls — Guard (vl-vardecllist-p vardecls).; assigns — Guard (vl-assignlist-p assigns).
Returns: new-stmt — Type (vl-edgesynth-stmt-p new-stmt), given (and (force (vl-expr-p condition)) (force (vl-edgesynth-stmt-p true-branch)) (force (vl-edgesynth-stmt-p false-branch)) (force (vl-atomicstmt-p true-branch)) (force (vl-atomicstmt-p false-branch))) .; nf — Type (vl-namefactory-p nf), given (force (vl-namefactory-p nf)).; vardecls — Type (vl-vardecllist-p vardecls), given the guard.; assigns — Type (vl-assignlist-p assigns), given the guard.

Assumption: any assignments are to the same register.

Definitions and Theorems

Function: vl-edgesynth-merge-data-ifs

(defun vl-edgesynth-merge-data-ifs
       (condition true-branch
                  false-branch nf vardecls assigns)
 (declare
      (xargs :guard (and (vl-expr-p condition)
                         (and (vl-stmt-p true-branch)
                              (vl-atomicstmt-p true-branch)
                              (vl-edgesynth-stmt-p true-branch))
                         (and (vl-stmt-p false-branch)
                              (vl-atomicstmt-p false-branch)
                              (vl-edgesynth-stmt-p false-branch))
                         (vl-namefactory-p nf)
                         (vl-vardecllist-p vardecls)
                         (vl-assignlist-p assigns))))
 (let ((__function__ 'vl-edgesynth-merge-data-ifs))
  (declare (ignorable __function__))
  (b* (((when (and (vl-nullstmt-p true-branch)
                   (vl-nullstmt-p false-branch)))
        (mv true-branch nf vardecls assigns))
       (base-assign (if (vl-assignstmt-p true-branch)
                        true-branch
                      false-branch))
       (target-reg (vl-assignstmt->lvalue base-assign))
       (loc (vl-assignstmt->loc base-assign))
       (width (vl-expr->finalwidth target-reg))
       (true-rhs (if (vl-assignstmt-p true-branch)
                     (vl-assignstmt->expr true-branch)
                   target-reg))
       (false-rhs (if (vl-assignstmt-p false-branch)
                      (vl-assignstmt->expr false-branch)
                    target-reg))
       (basename (cat (vl-idexpr->name target-reg)
                      "_next"))
       ((mv true-name nf)
        (vl-namefactory-indexed-name basename nf))
       ((mv false-name nf)
        (vl-namefactory-indexed-name basename nf))
       ((mv true-expr true-decl)
        (vl-occform-mkwire true-name width
                           :loc loc))
       ((mv false-expr false-decl)
        (vl-occform-mkwire false-name width
                           :loc loc))
       (true-assign (make-vl-assign :lvalue true-expr
                                    :expr true-rhs
                                    :loc loc))
       (false-assign (make-vl-assign :lvalue false-expr
                                     :expr false-rhs
                                     :loc loc))
       (vardecls (list* true-decl false-decl vardecls))
       (assigns (list* true-assign false-assign assigns))
       (new-rhs (vl-safe-qmark-expr condition true-expr false-expr))
       (new-stmt (change-vl-assignstmt base-assign
                                       :expr new-rhs)))
    (mv new-stmt nf vardecls assigns))))

Theorem: vl-edgesynth-stmt-p-of-vl-edgesynth-merge-data-ifs.new-stmt

(defthm vl-edgesynth-stmt-p-of-vl-edgesynth-merge-data-ifs.new-stmt
  (implies (and (force (vl-expr-p condition))
                (force (vl-edgesynth-stmt-p true-branch))
                (force (vl-edgesynth-stmt-p false-branch))
                (force (vl-atomicstmt-p true-branch))
                (force (vl-atomicstmt-p false-branch)))
           (b* (((mv ?new-stmt ?nf ?vardecls ?assigns)
                 (vl-edgesynth-merge-data-ifs
                      condition true-branch
                      false-branch nf vardecls assigns)))
             (vl-edgesynth-stmt-p new-stmt)))
  :rule-classes :rewrite)

Theorem: vl-namefactory-p-of-vl-edgesynth-merge-data-ifs.nf

(defthm vl-namefactory-p-of-vl-edgesynth-merge-data-ifs.nf
  (implies (force (vl-namefactory-p nf))
           (b* (((mv ?new-stmt ?nf ?vardecls ?assigns)
                 (vl-edgesynth-merge-data-ifs
                      condition true-branch
                      false-branch nf vardecls assigns)))
             (vl-namefactory-p nf)))
  :rule-classes :rewrite)

Theorem: vl-vardecllist-p-of-vl-edgesynth-merge-data-ifs.vardecls

(defthm vl-vardecllist-p-of-vl-edgesynth-merge-data-ifs.vardecls
  (implies (and (force (vl-expr-p condition))
                (force (if (vl-stmt-p true-branch)
                           (if (vl-atomicstmt-p true-branch)
                               (vl-edgesynth-stmt-p true-branch)
                             'nil)
                         'nil))
                (force (if (vl-stmt-p false-branch)
                           (if (vl-atomicstmt-p false-branch)
                               (vl-edgesynth-stmt-p false-branch)
                             'nil)
                         'nil))
                (force (vl-namefactory-p nf))
                (force (vl-vardecllist-p vardecls))
                (force (vl-assignlist-p assigns)))
           (b* (((mv ?new-stmt ?nf ?vardecls ?assigns)
                 (vl-edgesynth-merge-data-ifs
                      condition true-branch
                      false-branch nf vardecls assigns)))
             (vl-vardecllist-p vardecls)))
  :rule-classes :rewrite)

Theorem: vl-assignlist-p-of-vl-edgesynth-merge-data-ifs.assigns

(defthm vl-assignlist-p-of-vl-edgesynth-merge-data-ifs.assigns
  (implies (and (force (vl-expr-p condition))
                (force (if (vl-stmt-p true-branch)
                           (if (vl-atomicstmt-p true-branch)
                               (vl-edgesynth-stmt-p true-branch)
                             'nil)
                         'nil))
                (force (if (vl-stmt-p false-branch)
                           (if (vl-atomicstmt-p false-branch)
                               (vl-edgesynth-stmt-p false-branch)
                             'nil)
                         'nil))
                (force (vl-namefactory-p nf))
                (force (vl-vardecllist-p vardecls))
                (force (vl-assignlist-p assigns)))
           (b* (((mv ?new-stmt ?nf ?vardecls ?assigns)
                 (vl-edgesynth-merge-data-ifs
                      condition true-branch
                      false-branch nf vardecls assigns)))
             (vl-assignlist-p assigns)))
  :rule-classes :rewrite)