		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-module-edgesynth

Synthesize edge-triggered always blocks in a module.

Signature
(vl-module-edgesynth x &key vecp) → (mv new-x addmods)
Arguments: x — Guard (vl-module-p x).
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-edgesynth-fn

(defun vl-module-edgesynth-fn (x vecp)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-edgesynth))
  (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-edgesynth-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-edgesynth-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-alwayslist-edgesynth x.alwayses
                              scary-regs x.vardecls cvtregs delta
                              :vecp 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-edgesynth.new-x

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

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

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