		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-flatten-data-ifs

Flatten out bottom-level if tests about data signals, such as if (data-expr) q <= d1 else q <= d2 into assignments like q <= data-expr ? d1 : d2.

Signature
(vl-edgesynth-flatten-data-ifs x edgetable nf vardecls assigns) → (mv new-stmt nf vardecls assigns)
Arguments: x — Guard (and (vl-stmt-p x) (vl-edgesynth-stmt-p x)).; edgetable — Guard (vl-edgetable-p edgetable).; 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 (force (vl-edgesynth-stmt-p x)).; nf — Type (vl-namefactory-p nf), given (and (force (vl-edgesynth-stmt-p x)) (force (vl-namefactory-p nf))).

This is a best-effort transform that leaves the statement alone when it's not supported.

Originally I tried to just fail when the sizes of the true/false branch didn't line up, but that caused problems because sometimes we would see things like:

if (data-expr)
   q <= d1;
else
   q <= 0;

And the plain integers are badly sized. To deal with this, we now go ahead and do the work of introducing temporary wires as necessary. The only lousy part of this is that we can't really extend the vl-delta-p, since we're not sure everything's going to work out yet.

Definitions and Theorems

Function: vl-edgesynth-flatten-data-ifs

(defun vl-edgesynth-flatten-data-ifs
       (x edgetable nf vardecls assigns)
 (declare (xargs :guard (and (and (vl-stmt-p x)
                                  (vl-edgesynth-stmt-p x))
                             (vl-edgetable-p edgetable)
                             (vl-namefactory-p nf)
                             (vl-vardecllist-p vardecls)
                             (vl-assignlist-p assigns))))
 (let ((__function__ 'vl-edgesynth-flatten-data-ifs))
  (declare (ignorable __function__))
  (b*
   (((when (vl-atomicstmt-p x))
     (mv x nf vardecls assigns))
    ((when (vl-ifstmt-p x))
     (b* (((vl-ifstmt x) x)
          ((mv type ?guts)
           (vl-edgesynth-classify-iftest x.condition edgetable))
          ((mv true nf vardecls assigns)
           (vl-edgesynth-flatten-data-ifs
                x.truebranch
                edgetable nf vardecls assigns))
          ((mv false nf vardecls assigns)
           (vl-edgesynth-flatten-data-ifs
                x.falsebranch
                edgetable nf vardecls assigns))
          ((unless (and (equal type :data)
                        (vl-atomicstmt-p true)
                        (vl-atomicstmt-p false)))
           (mv (change-vl-ifstmt x
                                 :truebranch true
                                 :falsebranch false)
               nf vardecls assigns)))
      (vl-edgesynth-merge-data-ifs x.condition
                                   true false nf vardecls assigns)))
    ((when (vl-blockstmt-p x))
     (raise "Thought we already got rid of block statements!")
     (mv x nf vardecls assigns)))
   (raise "Should be impossible.")
   (mv x nf vardecls assigns))))

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

(defthm
      vl-edgesynth-stmt-p-of-vl-edgesynth-flatten-data-ifs.new-stmt
  (implies (force (vl-edgesynth-stmt-p x))
           (b* (((mv ?new-stmt ?nf ?vardecls ?assigns)
                 (vl-edgesynth-flatten-data-ifs
                      x edgetable nf vardecls assigns)))
             (vl-edgesynth-stmt-p new-stmt)))
  :rule-classes :rewrite)

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

(defthm vl-namefactory-p-of-vl-edgesynth-flatten-data-ifs.nf
  (implies (and (force (vl-edgesynth-stmt-p x))
                (force (vl-namefactory-p nf)))
           (b* (((mv ?new-stmt ?nf ?vardecls ?assigns)
                 (vl-edgesynth-flatten-data-ifs
                      x edgetable nf vardecls assigns)))
             (vl-namefactory-p nf)))
  :rule-classes :rewrite)

Theorem: vl-edgesynth-flatten-data-ifs-basics

(defthm vl-edgesynth-flatten-data-ifs-basics
  (implies (and (force (vl-edgesynth-stmt-p x))
                (force (vl-namefactory-p nf))
                (force (vl-vardecllist-p vardecls))
                (force (vl-assignlist-p assigns)))
           (b* (((mv ?new-x ?nf ?vardecls ?assigns)
                 (vl-edgesynth-flatten-data-ifs
                      x edgetable nf vardecls assigns)))
             (and (vl-vardecllist-p vardecls)
                  (vl-assignlist-p assigns)))))