		Search-engine friendly clone of the ACL2 documentation.

Vl-match-posedge-clk

Match always @(posedge clk) body.

Signature
(vl-match-posedge-clk x) → (mv clk body)
Arguments: x — Guard (vl-always-p x).
Returns: clk — Type (equal (vl-expr-p clk) (if clk t nil)).; body — Type (equal (vl-stmt-p body) (if clk t nil)).

Definitions and Theorems

Function: vl-match-posedge-clk

(defun vl-match-posedge-clk (x)
  (declare (xargs :guard (vl-always-p x)))
  (let ((__function__ 'vl-match-posedge-clk))
    (declare (ignorable __function__))
    (b* ((stmt (vl-always->stmt x))
         ((unless (eq (vl-stmt-kind stmt) :vl-timingstmt))
          (mv nil nil))
         ((vl-timingstmt stmt) stmt)
         ((unless (and (eq (tag stmt.ctrl) :vl-eventcontrol)
                       (not (vl-eventcontrol->starp stmt.ctrl))))
          (mv nil nil))
         (evatoms (vl-eventcontrol->atoms stmt.ctrl))
         ((unless (and (eql (len evatoms) 1)
                       (eq (vl-evatom->type (car evatoms))
                           :vl-posedge)))
          (mv nil nil))
         (clk (vl-evatom->expr (car evatoms))))
      (mv clk stmt.body))))

Theorem: return-type-of-vl-match-posedge-clk.clk

(defthm return-type-of-vl-match-posedge-clk.clk
  (b* (((mv ?clk ?body)
        (vl-match-posedge-clk x)))
    (equal (vl-expr-p clk) (if clk t nil)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-match-posedge-clk.body

(defthm return-type-of-vl-match-posedge-clk.body
  (b* (((mv ?clk ?body)
        (vl-match-posedge-clk x)))
    (equal (vl-stmt-p body) (if clk t nil)))
  :rule-classes :rewrite)

Theorem: vl-match-posedge-clk-of-vl-always-fix-x

(defthm vl-match-posedge-clk-of-vl-always-fix-x
  (equal (vl-match-posedge-clk (vl-always-fix x))
         (vl-match-posedge-clk x)))

Theorem: vl-match-posedge-clk-vl-always-equiv-congruence-on-x

(defthm vl-match-posedge-clk-vl-always-equiv-congruence-on-x
  (implies (vl-always-equiv x x-equiv)
           (equal (vl-match-posedge-clk x)
                  (vl-match-posedge-clk x-equiv)))
  :rule-classes :congruence)