		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-pattern-match

Recognize basic if statements for the core of a multi-edge block: we're basically looking for a proper priority ordering on the edges.

Signature
(vl-edgesynth-pattern-match target x edgetable) → (mv okp clks rhses final-rhs)
Arguments: target — Guard (vl-expr-p target).; x — Guard (and (vl-stmt-p x) (vl-edgesynth-stmt-p x)).; edgetable — Guard (vl-edgetable-p edgetable).
Returns: okp — Type (booleanp okp).; clks — Names of clocks in priority order.
Type (string-listp clks).; rhses — Corresponding right hand sides.
Type (vl-exprlist-p rhses), given the guard.; final-rhs — Right-hand side for the final else statement.
Type (vl-expr-p final-rhs), given the guard.

We're not trying to do much sanity checking here. We just want to match x against a basic template like:

if (clk1) assign1;
else if (clk2) null;
else if (clk3) assign3;
finally;

All if-tests that we match for clocks have the proper polarity for their corresponding edges.

Definitions and Theorems

Function: vl-edgesynth-pattern-match

(defun vl-edgesynth-pattern-match (target x edgetable)
 (declare (xargs :guard (and (vl-expr-p target)
                             (and (vl-stmt-p x)
                                  (vl-edgesynth-stmt-p x))
                             (vl-edgetable-p edgetable))))
 (let ((__function__ 'vl-edgesynth-pattern-match))
  (declare (ignorable __function__))
  (b*
   (((when (vl-nullstmt-p x))
     (mv t nil nil target))
    ((when (vl-assignstmt-p x))
     (mv t nil nil (vl-assignstmt->expr x)))
    ((unless (vl-ifstmt-p x))
     (mv nil nil nil target))
    ((vl-ifstmt x) x)
    ((mv type guts)
     (vl-edgesynth-classify-iftest x.condition edgetable))
    ((when (eq type :clock))
     (b*
      ((clockname (vl-idexpr->name guts))
       (edge (cdr (hons-assoc-equal clockname edgetable)))
       (posedgep (vl-edgesynth-edge->posedgep edge))
       ((unless posedgep)
        (mv nil nil nil target))
       ((unless (vl-atomicstmt-p x.truebranch))
        (mv nil nil nil target))
       ((mv okp clks rhses finally)
        (vl-edgesynth-pattern-match target x.falsebranch edgetable))
       ((unless okp) (mv nil nil nil target))
       (rhs (if (vl-nullstmt-p x.truebranch)
                target
              (vl-assignstmt->expr x.truebranch))))
      (mv t (cons clockname clks)
          (cons rhs rhses)
          finally)))
    ((when (eq type :nclock))
     (b*
      ((clockname (vl-idexpr->name guts))
       (edge (cdr (hons-assoc-equal clockname edgetable)))
       (posedgep (vl-edgesynth-edge->posedgep edge))
       ((when posedgep)
        (mv nil nil nil target))
       ((unless (vl-atomicstmt-p x.truebranch))
        (mv nil nil nil target))
       ((mv okp clks rhses finally)
        (vl-edgesynth-pattern-match target x.falsebranch edgetable))
       ((unless okp) (mv nil nil nil target))
       (rhs (if (vl-nullstmt-p x.truebranch)
                target
              (vl-assignstmt->expr x.truebranch))))
      (mv t (cons clockname clks)
          (cons rhs rhses)
          finally))))
   (mv nil nil nil target))))

Theorem: booleanp-of-vl-edgesynth-pattern-match.okp

(defthm booleanp-of-vl-edgesynth-pattern-match.okp
  (b* (((mv ?okp ?clks ?rhses ?final-rhs)
        (vl-edgesynth-pattern-match target x edgetable)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: string-listp-of-vl-edgesynth-pattern-match.clks

(defthm string-listp-of-vl-edgesynth-pattern-match.clks
  (b* (((mv ?okp ?clks ?rhses ?final-rhs)
        (vl-edgesynth-pattern-match target x edgetable)))
    (string-listp clks))
  :rule-classes :rewrite)

Theorem: vl-exprlist-p-of-vl-edgesynth-pattern-match.rhses

(defthm vl-exprlist-p-of-vl-edgesynth-pattern-match.rhses
  (implies (and (vl-expr-p target)
                (if (vl-stmt-p x)
                    (vl-edgesynth-stmt-p x)
                  'nil)
                (vl-edgetable-p edgetable))
           (b* (((mv ?okp ?clks ?rhses ?final-rhs)
                 (vl-edgesynth-pattern-match target x edgetable)))
             (vl-exprlist-p rhses)))
  :rule-classes :rewrite)

Theorem: vl-expr-p-of-vl-edgesynth-pattern-match.final-rhs

(defthm vl-expr-p-of-vl-edgesynth-pattern-match.final-rhs
  (implies (and (vl-expr-p target)
                (if (vl-stmt-p x)
                    (vl-edgesynth-stmt-p x)
                  'nil)
                (vl-edgetable-p edgetable))
           (b* (((mv ?okp ?clks ?rhses ?final-rhs)
                 (vl-edgesynth-pattern-match target x edgetable)))
             (vl-expr-p final-rhs)))
  :rule-classes :rewrite)

Theorem: vl-edgesynth-pattern-match-mvtypes-1

(defthm vl-edgesynth-pattern-match-mvtypes-1
  (true-listp
       (mv-nth 1
               (vl-edgesynth-pattern-match target x edgetable)))
  :rule-classes :type-prescription)

Theorem: vl-edgesynth-pattern-match-mvtypes-2

(defthm vl-edgesynth-pattern-match-mvtypes-2
  (true-listp
       (mv-nth 2
               (vl-edgesynth-pattern-match target x edgetable)))
  :rule-classes :type-prescription)