		Search-engine friendly clone of the ACL2 documentation.

Latchcode

Vl-match-latch-main

Pattern matcher for always blocks that might be simple latches.

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

We match always blocks of two forms. Note that form1 is generally preferable to form2 since if statements behave very badly when test is X or Z.

// form 1                             // form 2
always @(x or y or z or ...)          always @(x or y or z or ...)
  lhs = [#delay] test ? rhs : lhs;      if (test) lhs = [#delay] rhs;

We do not check many things here: see vl-careful-match-latch versus vl-careless-match-latch. However, we do at least make sure that the sensitivity list has only plain atoms, i.e., posedge/negedge are not allowed.

We previously allowed blocking or non-blocking assignments, but we now require that blocking assignments. Blocking assignments appear to be the correct Verilog coding style for always blocks that aren't edge-triggered; see for instance Cliff Cummings articles about coding styles for non-blocking assignments.

Definitions and Theorems

Function: vl-match-latch-main

(defun vl-match-latch-main (x)
 (declare (xargs :guard (vl-always-p x)))
 (let ((__function__ 'vl-match-latch-main))
   (declare (ignorable __function__))
   (b*
    ((stmt (vl-always->stmt x))
     ((unless (vl-timingstmt-p stmt))
      (mv nil nil nil nil nil))
     ((vl-timingstmt stmt) stmt)
     ((unless (and (mbe :logic (vl-eventcontrol-p stmt.ctrl)
                        :exec (eq (tag stmt.ctrl) :vl-eventcontrol))
                   (or (vl-eventcontrol->starp stmt.ctrl)
                       (vl-evatomlist-plain-p
                            (vl-eventcontrol->atoms stmt.ctrl)))))
      (mv nil nil nil nil nil))
     ((mv condition lhs rhs delay)
      (vl-match-latchbody stmt.body))
     ((unless condition)
      (mv nil nil nil nil nil)))
    (mv stmt.ctrl condition lhs rhs delay))))

Theorem: return-type-of-vl-match-latch-main.ctrl

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

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

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

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

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

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

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

Theorem: plain-evatoms-when-vl-match-latch-main

(defthm plain-evatoms-when-vl-match-latch-main
 (implies
    (force (vl-always-p x))
    (b* (((mv ctrl ?condition ?lhs ?rhs)
          (vl-match-latch-main x)))
      (implies
           (and ctrl
                (not (vl-eventcontrol->starp ctrl)))
           (vl-evatomlist-plain-p (vl-eventcontrol->atoms ctrl))))))

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

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

Subtopics

Vl-match-latchbody-form2: Match if (test) lhs = [#delay] rhs.
Vl-match-latchbody-form1: Match lhs = [#delay] test ? rhs : lhs.
Vl-evatom-plain-p: We say a vl-evatom-p is plain when it has no posedge or negedge, and the expression is a simple identifier. For instance, an event control list like @(a or b or c) contains only plain evatoms.
Vl-match-latchbody: Pattern match simple kinds of latch statements.
Vl-evatomlist-plain-p: (vl-evatomlist-plain-p x) recognizes lists where every element satisfies vl-evatom-plain-p.