		Search-engine friendly clone of the ACL2 documentation.

Latchcode

Vl-careless-match-latch

Match always statements that are simple latches, with minimal sanity checking.

Signature
(vl-careless-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)) (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-careless-match-latch

(defun vl-careless-match-latch (x warnings)
 (declare (xargs :guard (and (vl-always-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-careless-match-latch))
  (declare (ignorable __function__))
  (b*
   (((mv ctrl condition lhs rhs delay)
     (vl-match-latch-main x))
    ((unless ctrl)
     (mv warnings nil nil nil nil))
    ((vl-eventcontrol ctrl) ctrl)
    (lhs-wires (mergesort (vl-expr-names lhs)))
    (rhs-wires (mergesort (vl-expr-names rhs)))
    (condition-wires (mergesort (vl-expr-names condition)))
    (lhs/rhs-overlap (intersect lhs-wires rhs-wires))
    (warnings
     (if lhs/rhs-overlap
      (warn
       :type :vl-warn-loopy-latch
       :msg
       "~a0: some wires on the left-hand side of the latch ~
                        are also mentioned in the rhs, which might mean a ~
                        combinational loop when the latch is enabled. Loopy ~
                        wires: ~&1."
       :args (list x lhs/rhs-overlap))
      warnings))
    (lhs/condition-overlap (intersect lhs-wires condition-wires))
    (warnings
     (if lhs/condition-overlap
      (warn
       :type :vl-warn-weird-latch
       :msg
       "~a0: some wires on the left-hand side of the latch ~
                        are also mentioned in the enable condition, which is ~
                        strange and might indicate some kind of weird race.  ~
                        Wires: ~&1."
       :args (list x lhs/condition-overlap))
      warnings))
    (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-careless-match-latch.warnings

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

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

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

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

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

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

(defthm return-type-of-vl-careless-match-latch.rhs
  (implies (and (force (vl-always-p x))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?test ?lhs ?rhs ?delay)
                 (vl-careless-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-careless-match-latch.ticks

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