		Search-engine friendly clone of the ACL2 documentation.

Always-top

Vl-stmt-guts

Coerce a statement into a statement list.

Signature
(vl-stmt-guts body) → guts
Arguments: body — Guard (vl-stmt-p body).
Returns: guts — Type (vl-stmtlist-p guts).

The idea here is to be able to treat things like these:

always @(posedge clk)   vs.  always @(posedge clk)
  lhs <= rhs;                  begin
                                 lhs <= rhs;
                               end

in a uniform way. If we see a begin ... end we'll just return the ... part as a statement list. If we see any other kind of statement, e.g., an if statement, a single assignment, etc., then we just return it as a singleton statement list.

Definitions and Theorems

Function: vl-stmt-guts

(defun vl-stmt-guts (body)
  (declare (xargs :guard (vl-stmt-p body)))
  (let ((__function__ 'vl-stmt-guts))
    (declare (ignorable __function__))
    (if (and (eq (vl-stmt-kind body) :vl-blockstmt)
             (vl-blockstmt->sequentialp body)
             (not (vl-blockstmt->vardecls body))
             (not (vl-blockstmt->paramdecls body)))
        (vl-blockstmt->stmts body)
      (list (vl-stmt-fix body)))))

Theorem: vl-stmtlist-p-of-vl-stmt-guts

(defthm vl-stmtlist-p-of-vl-stmt-guts
  (b* ((guts (vl-stmt-guts body)))
    (vl-stmtlist-p guts))
  :rule-classes :rewrite)

Theorem: vl-stmt-guts-of-vl-stmt-fix-body

(defthm vl-stmt-guts-of-vl-stmt-fix-body
  (equal (vl-stmt-guts (vl-stmt-fix body))
         (vl-stmt-guts body)))

Theorem: vl-stmt-guts-vl-stmt-equiv-congruence-on-body

(defthm vl-stmt-guts-vl-stmt-equiv-congruence-on-body
  (implies (vl-stmt-equiv body body-equiv)
           (equal (vl-stmt-guts body)
                  (vl-stmt-guts body-equiv)))
  :rule-classes :congruence)