		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-blockelim

Eliminate begin/end blocks and leave us with just an IF structure.

Assumptions:

All assignments are to the same register (call it Q).
At least one assignment writes to Q.
All assignments have compatible delays.

Our goal is to eliminate any begin/end blocks and end up with just assignments, if statements, and null statements. For instance, we might rewrite:

begin                      if (clk1)
  q <= d3;       ----->       q <= d1;
  if (clk2)                else if (clk2)
     q <= d2;                 q <= d2;
  if (clk1)                else
     q <= d1;                 q <= d3;
end

Definitions and Theorems

Function: vl-edgesynth-stmt-blockelim

(defun vl-edgesynth-stmt-blockelim (x curr)
 (declare (xargs :guard (and (and (vl-stmt-p x)
                                  (vl-edgesynth-stmt-p x))
                             (and (vl-stmt-p curr)
                                  (vl-edgesynth-stmt-p curr)))))
 (let ((__function__ 'vl-edgesynth-stmt-blockelim))
   (declare (ignorable __function__))
   (b*
    (((when (vl-nullstmt-p x)) curr)
     ((when (vl-assignstmt-p x)) x)
     ((when (vl-ifstmt-p x))
      (b* (((vl-ifstmt x) x)
           (true (vl-edgesynth-stmt-blockelim x.truebranch curr))
           (false (vl-edgesynth-stmt-blockelim x.falsebranch curr)))
        (change-vl-ifstmt x
                          :truebranch true
                          :falsebranch false)))
     ((when (vl-blockstmt-p x))
      (b* (((vl-blockstmt x) x))
        (vl-edgesynth-stmtlist-blockelim x.stmts curr))))
    curr)))

Function: vl-edgesynth-stmtlist-blockelim

(defun vl-edgesynth-stmtlist-blockelim (x curr)
  (declare (xargs :guard (and (and (vl-stmtlist-p x)
                                   (vl-edgesynth-stmtlist-p x))
                              (and (vl-stmt-p curr)
                                   (vl-edgesynth-stmt-p curr)))))
  (let ((__function__ 'vl-edgesynth-stmtlist-blockelim))
    (declare (ignorable __function__))
    (b* (((when (atom x)) curr)
         (curr (vl-edgesynth-stmt-blockelim (car x)
                                            curr)))
      (vl-edgesynth-stmtlist-blockelim (cdr x)
                                       curr))))

Theorem: return-type-of-vl-edgesynth-stmt-blockelim.new-stmt

(defthm return-type-of-vl-edgesynth-stmt-blockelim.new-stmt
  (implies (and (force (if (vl-stmt-p x)
                           (vl-edgesynth-stmt-p x)
                         'nil))
                (force (vl-stmt-p curr))
                (force (vl-edgesynth-stmt-p curr)))
           (b* ((?new-stmt (vl-edgesynth-stmt-blockelim x curr)))
             (vl-edgesynth-stmt-p new-stmt)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-edgesynth-stmtlist-blockelim.stmts

(defthm return-type-of-vl-edgesynth-stmtlist-blockelim.stmts
  (implies (and (force (if (vl-stmtlist-p x)
                           (vl-edgesynth-stmtlist-p x)
                         'nil))
                (force (vl-stmt-p curr))
                (force (vl-edgesynth-stmt-p curr)))
           (b* ((?stmts (vl-edgesynth-stmtlist-blockelim x curr)))
             (vl-edgesynth-stmt-p stmts)))
  :rule-classes :rewrite)

Subtopics

Vl-edgesynth-stmt-blockelim
Vl-edgesynth-stmtlist-blockelim