		Search-engine friendly clone of the ACL2 documentation.

Stmttemps

Vl-always-stmttemps

Signature
(vl-always-stmttemps x delta) → (mv new-x delta)
Arguments: x — Guard (vl-always-p x).; delta — Guard (vl-delta-p delta).
Returns: new-x — Type (vl-always-p new-x), given the guard.; delta — Type (vl-delta-p delta), given the guard.

Definitions and Theorems

Function: vl-always-stmttemps

(defun vl-always-stmttemps (x delta)
  (declare (xargs :guard (and (vl-always-p x)
                              (vl-delta-p delta))))
  (let ((__function__ 'vl-always-stmttemps))
    (declare (ignorable __function__))
    (b* (((vl-always x) x)
         ((mv clk ?body)
          (vl-match-posedge-clk x))
         ((unless clk) (mv x delta))
         ((mv stmt delta)
          (vl-stmt-stmttemps x.stmt delta x)))
      (mv (change-vl-always x :stmt stmt)
          delta))))

Theorem: vl-always-p-of-vl-always-stmttemps.new-x

(defthm vl-always-p-of-vl-always-stmttemps.new-x
  (implies (and (force (vl-always-p x))
                (force (vl-delta-p delta)))
           (b* (((mv ?new-x ?delta)
                 (vl-always-stmttemps x delta)))
             (vl-always-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-always-stmttemps.delta

(defthm vl-delta-p-of-vl-always-stmttemps.delta
  (implies (and (force (vl-always-p x))
                (force (vl-delta-p delta)))
           (b* (((mv ?new-x ?delta)
                 (vl-always-stmttemps x delta)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)