		Search-engine friendly clone of the ACL2 documentation.

Latchsynth

Vl-module-latchsynth

Synthesize simple latch-like always blocks in a module.

Signature
(vl-module-latchsynth x careful-p vecp) → (mv new-x addmods)
Arguments: x — Guard (vl-module-p x).; careful-p — be careful when processing latches?.
Guard (booleanp careful-p).
Returns: new-x — Type (vl-module-p new-x), given the guard.; addmods — Type (vl-modulelist-p addmods), given the guard.

Definitions and Theorems

Function: vl-module-latchsynth

(defun vl-module-latchsynth (x careful-p vecp)
 (declare (xargs :guard (and (vl-module-p x)
                             (booleanp careful-p))))
 (let ((__function__ 'vl-module-latchsynth))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    ((when (vl-module->hands-offp x))
     (mv x nil))
    ((unless (consp x.alwayses)) (mv x nil))
    ((when (consp x.taskdecls))
     (b*
      ((warnings
        (warn
         :type :vl-latchsynth-fail
         :msg
         "~m0 has tasks, so we are not going to try ~
                                   to synthesize its always blocks."
         :args (list x.name)
         :acc x.warnings)))
      (mv (change-vl-module x :warnings warnings)
          nil)))
    ((when (consp x.initials))
     (b*
      ((warnings
        (warn
         :type :vl-latchsynth-fail
         :msg
         "~m0 has initial statements so we aren't going to ~
                          try to synthesize its always blocks.  Note: usually ~
                          eliminitial should be run before edgesynth, in ~
                          which case you should not see this warning."
         :args (list x.name)
         :acc x.warnings)))
      (mv (change-vl-module x :warnings warnings)
          nil)))
    (delta (vl-starting-delta x))
    (delta (change-vl-delta delta
                            :modinsts x.modinsts
                            :assigns x.assigns))
    (scary-regs (vl-always-scary-regs x.alwayses))
    (cvtregs nil)
    ((mv new-alwayses cvtregs delta)
     (vl-latchcode-synth-alwayses x.alwayses scary-regs x.vardecls
                                  cvtregs delta careful-p vecp))
    ((vl-delta delta) (vl-free-delta delta))
    ((mv fixed-vardecls fixed-portdecls)
     (vl-convert-regs cvtregs x.vardecls x.portdecls))
    (final-vardecls
         (append-without-guard delta.vardecls fixed-vardecls))
    (new-x (change-vl-module x
                             :vardecls final-vardecls
                             :portdecls fixed-portdecls
                             :assigns delta.assigns
                             :modinsts delta.modinsts
                             :alwayses new-alwayses
                             :warnings delta.warnings)))
   (mv new-x delta.addmods))))

Theorem: vl-module-p-of-vl-module-latchsynth.new-x

(defthm vl-module-p-of-vl-module-latchsynth.new-x
  (implies (and (force (vl-module-p x))
                (force (booleanp careful-p)))
           (b* (((mv ?new-x ?addmods)
                 (vl-module-latchsynth x careful-p vecp)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-module-latchsynth.addmods

(defthm vl-modulelist-p-of-vl-module-latchsynth.addmods
  (implies (and (force (vl-module-p x))
                (force (booleanp careful-p)))
           (b* (((mv ?new-x ?addmods)
                 (vl-module-latchsynth x careful-p vecp)))
             (vl-modulelist-p addmods)))
  :rule-classes :rewrite)