		Search-engine friendly clone of the ACL2 documentation.

Always-top

Vl-always-check-reg

See if a register is simple enough to reasonably synthesize into a flop/latch.

Signature
(vl-always-check-reg name vars elem) → warning?
Arguments: name — name of a supposed register to be checked.
Guard (stringp name).; vars — all variables in the module.
Guard (vl-vardecllist-p vars).; elem — context for error messages.
Guard (vl-modelement-p elem).
Returns: warning? — Type (equal (vl-warning-p warning?) (if warning? t nil)).

We just make sure name is defined as a register and that it isn't an array.

Definitions and Theorems

Function: vl-always-check-reg

(defun vl-always-check-reg (name vars elem)
 (declare (xargs :guard (and (stringp name)
                             (vl-vardecllist-p vars)
                             (vl-modelement-p elem))))
 (let ((__function__ 'vl-always-check-reg))
  (declare (ignorable __function__))
  (b*
   ((name (string-fix name))
    (elem (vl-modelement-fix elem))
    (decl (vl-find-vardecl name vars))
    ((unless decl)
     (make-vl-warning
      :type :vl-always-too-hard
      :msg
      "~a0: statement is too complex to synthesize.  The variable ~
               being targeted, ~w1, is not declared as a register."
      :args (list elem name)
      :fatalp nil
      :fn __function__))
    ((unless (vl-simplereg-p decl))
     (make-vl-warning
      :type :vl-always-too-hard
      :msg
      "~a0: statement is too complex to synthesize.  The variable ~
               being targeted, ~w1, is not a simple enough register."
      :args (list elem name)
      :fatalp nil
      :fn __function__))
    (range (vl-simplereg->range decl))
    ((unless (vl-maybe-range-resolved-p range))
     (make-vl-warning
      :type :vl-always-too-hard
      :msg
      "~a0: statement is too complex to synthesize.  The register ~
               being targeted, ~w1, does not have a resolved size: ~x2"
      :args (list elem name range)
      :fatalp nil
      :fn __function__)))
   nil)))

Theorem: return-type-of-vl-always-check-reg

(defthm return-type-of-vl-always-check-reg
  (b* ((warning? (vl-always-check-reg name vars elem)))
    (equal (vl-warning-p warning?)
           (if warning? t nil)))
  :rule-classes :rewrite)

Theorem: reg-exists-unless-vl-always-check-reg

(defthm reg-exists-unless-vl-always-check-reg
  (implies (and (not (vl-always-check-reg name regs elem))
                (force (stringp name))
                (force (vl-vardecllist-p regs)))
           (member-equal name (vl-vardecllist->names regs))))

Theorem: vl-always-check-reg-of-str-fix-name

(defthm vl-always-check-reg-of-str-fix-name
  (equal (vl-always-check-reg (str-fix name)
                              vars elem)
         (vl-always-check-reg name vars elem)))

Theorem: vl-always-check-reg-streqv-congruence-on-name

(defthm vl-always-check-reg-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-always-check-reg name vars elem)
                  (vl-always-check-reg name-equiv vars elem)))
  :rule-classes :congruence)

Theorem: vl-always-check-reg-of-vl-vardecllist-fix-vars

(defthm vl-always-check-reg-of-vl-vardecllist-fix-vars
  (equal (vl-always-check-reg name (vl-vardecllist-fix vars)
                              elem)
         (vl-always-check-reg name vars elem)))

Theorem: vl-always-check-reg-vl-vardecllist-equiv-congruence-on-vars

(defthm vl-always-check-reg-vl-vardecllist-equiv-congruence-on-vars
  (implies (vl-vardecllist-equiv vars vars-equiv)
           (equal (vl-always-check-reg name vars elem)
                  (vl-always-check-reg name vars-equiv elem)))
  :rule-classes :congruence)

Theorem: vl-always-check-reg-of-vl-modelement-fix-elem

(defthm vl-always-check-reg-of-vl-modelement-fix-elem
  (equal (vl-always-check-reg name vars (vl-modelement-fix elem))
         (vl-always-check-reg name vars elem)))

Theorem: vl-always-check-reg-vl-modelement-equiv-congruence-on-elem

(defthm vl-always-check-reg-vl-modelement-equiv-congruence-on-elem
  (implies (vl-modelement-equiv elem elem-equiv)
           (equal (vl-always-check-reg name vars elem)
                  (vl-always-check-reg name vars elem-equiv)))
  :rule-classes :congruence)