		Search-engine friendly clone of the ACL2 documentation.

Cblock-path-checking

Vl-cblock-synth

Should only be called on good cblocks.

Signature
(vl-cblock-synth x vars delta) → (mv delta cvtregs)
Arguments: x — Guard (vl-always-p x).; vars — Guard (vl-vardecllist-p vars).; delta — Guard (vl-delta-p delta).
Returns: delta — Type (vl-delta-p delta), given the guard.; cvtregs — Type (string-listp cvtregs).

Definitions and Theorems

Function: vl-cblock-synth

(defun vl-cblock-synth (x vars delta)
 (declare (xargs :guard (and (vl-always-p x)
                             (vl-vardecllist-p vars)
                             (vl-delta-p delta))))
 (let ((__function__ 'vl-cblock-synth))
  (declare (ignorable __function__))
  (b*
   ((stmt (vl-always->stmt x))
    (type (vl-always->type x))
    ((mv okp ctrl body)
     (cond ((eq type :vl-always-comb)
            (mv t nil stmt))
           ((and (eq type :vl-always)
                 (vl-timingstmt-p stmt))
            (mv t (vl-timingstmt->ctrl stmt)
                (vl-timingstmt->body stmt)))
           (t (mv nil nil nil))))
    ((unless okp)
     (raise "Not a valid cblock: ~x0." x)
     (mv delta nil))
    ((unless (and (or (eq type :vl-always-comb)
                      (vl-star-control-p ctrl)
                      (vl-classic-control-p ctrl))
                  (vl-stmt-cblock-p body)))
     (raise "Not a valid cblock: ~x0." x)
     (mv delta nil))
    ((mv body delta)
     (vl-stmt-stmttemps body delta x))
    ((unless (vl-stmt-cblock-p body))
     (raise "Somehow stmttemps screwed up the body?"
            x)
     (mv delta nil))
    (lvalues
       (mergesort
            (vl-idexprlist->names (vl-stmt-cblock-lvalexprs body))))
    (assigns (vl-cblock-make-assigns lvalues vars body x))
    (delta
         (change-vl-delta
              delta
              :assigns (append assigns (vl-delta->assigns delta)))))
   (mv delta lvalues))))

Theorem: vl-delta-p-of-vl-cblock-synth.delta

(defthm vl-delta-p-of-vl-cblock-synth.delta
  (implies (and (force (vl-always-p x))
                (force (vl-vardecllist-p vars))
                (force (vl-delta-p delta)))
           (b* (((mv ?delta ?cvtregs)
                 (vl-cblock-synth x vars delta)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-cblock-synth.cvtregs

(defthm string-listp-of-vl-cblock-synth.cvtregs
  (b* (((mv ?delta ?cvtregs)
        (vl-cblock-synth x vars delta)))
    (string-listp cvtregs))
  :rule-classes :rewrite)