		Search-engine friendly clone of the ACL2 documentation.

Latchcode

Vl-careful-match-latch

Match always statements that are simple latches, with lots of extra sanity checking.

Signature
(vl-careful-match-latch x warnings) → (mv warnings test lhs rhs delay)
Arguments: x — Guard (vl-always-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings), given the guard.; test — Type (equal (vl-expr-p test) (if test t nil)), given the guard.; lhs — Type (and (equal (vl-expr-p lhs) (if test t nil)) (equal (vl-idexpr-p lhs) (if test t nil)) (iff lhs test)) , given the guard.; rhs — Type (and (equal (vl-expr-p rhs) (if test t nil)) (iff rhs test)), given the guard.; delay — maybe natp.

Definitions and Theorems

Function: vl-careful-match-latch

(defun vl-careful-match-latch (x warnings)
 (declare (xargs :guard (and (vl-always-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-careful-match-latch))
  (declare (ignorable __function__))
  (b*
   (((mv ctrl condition lhs rhs delay)
     (vl-match-latch-main x))
    ((unless (and ctrl (vl-idexpr-p lhs)))
     (mv warnings nil nil nil nil))
    ((unless (vl-idexpr-p lhs))
     (mv
      (warn
       :type :vl-latch-fail
       :msg
       "~a0: failing to infer a latch because the left-hand ~
                        side, ~a1, isn't a simple identifier."
       :args (list x lhs))
      nil nil nil nil))
    ((vl-eventcontrol ctrl) ctrl)
    (lhs-name (vl-idexpr->name lhs))
    (rhs-wires (vl-expr-names rhs))
    (condition-wires (vl-expr-names condition))
    ((when (member-equal lhs-name rhs-wires))
     (mv
      (warn
       :type :vl-latch-fail
       :msg
       "~a0: failing to infer a latch because the register ~
                        being assigned to, ~s1, occurs in the rhs expression, ~
                        ~a2.  This suggests there may be a combinational loop ~
                        when the latch is enabled."
       :args (list x lhs-name rhs))
      nil nil nil nil))
    ((when (member-equal lhs-name condition-wires))
     (mv
      (warn
       :type :vl-latch-fail
       :msg
       "~a0: failing to infer a latch because the register ~
                        being assigned to, ~s1, occurs in its own enable ~
                        expression, ~a2.  This seems very strange and might ~
                        indicate some kind of weird race."
       :args (list x lhs-name condition))
      nil nil nil nil))
    (need-wires (if ctrl.starp nil
                  (append rhs-wires condition-wires)))
    (have-wires
        (if ctrl.starp nil
          (vl-idexprlist->names (vl-evatomlist->exprs ctrl.atoms))))
    ((unless (subsetp-equal need-wires have-wires))
     (mv
      (warn
       :type :vl-latch-fail
       :msg
       "~a0: failing to infer a latch since the sensitivity ~
                        list omits ~&1."
       :args (list x
                   (set-difference-equal need-wires have-wires)))
      nil nil nil nil))
    (warnings
     (if (subsetp-equal have-wires need-wires)
         warnings
      (warn
       :type :vl-sensitivity-list
       :msg
       "~a0: sensitivity list appears to include ~&1 ~
                      unnecessarily, which might slow down simulations."
       :args (list x
                   (set-difference-equal have-wires need-wires))))))
   (mv warnings condition lhs rhs delay))))

Theorem: vl-warninglist-p-of-vl-careful-match-latch.warnings

(defthm vl-warninglist-p-of-vl-careful-match-latch.warnings
  (implies (and (force (vl-always-p x))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?test ?lhs ?rhs ?delay)
                 (vl-careful-match-latch x warnings)))
             (vl-warninglist-p warnings)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-careful-match-latch.test

(defthm return-type-of-vl-careful-match-latch.test
  (implies (and (force (vl-always-p x))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?test ?lhs ?rhs ?delay)
                 (vl-careful-match-latch x warnings)))
             (equal (vl-expr-p test)
                    (if test t nil))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-careful-match-latch.lhs

(defthm return-type-of-vl-careful-match-latch.lhs
  (implies (and (force (vl-always-p x))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?test ?lhs ?rhs ?delay)
                 (vl-careful-match-latch x warnings)))
             (and (equal (vl-expr-p lhs) (if test t nil))
                  (equal (vl-idexpr-p lhs)
                         (if test t nil))
                  (iff lhs test))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-careful-match-latch.rhs

(defthm return-type-of-vl-careful-match-latch.rhs
  (implies (and (force (vl-always-p x))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?test ?lhs ?rhs ?delay)
                 (vl-careful-match-latch x warnings)))
             (and (equal (vl-expr-p rhs) (if test t nil))
                  (iff rhs test))))
  :rule-classes :rewrite)

Theorem: maybe-natp-of-vl-careful-match-latch.ticks

(defthm maybe-natp-of-vl-careful-match-latch.ticks
  (maybe-natp (mv-nth 4 (vl-careful-match-latch x warnings)))
  :rule-classes :type-prescription)