		Search-engine friendly clone of the ACL2 documentation.

Always-top

Vl-design-always-backend

Normal way to process always blocks after sizing.

Signature
(vl-design-always-backend x &key (careful-p 't) vecp) → new-x
Arguments: x — Guard (vl-design-p x).; careful-p — Guard (booleanp careful-p).
Returns: new-x — Type (vl-design-p new-x).

This is a combination of several other transforms. It is the typical way that we expect to process always blocks.

Modules that survive this transform will be free of always blocks—or, well, that's true except for the primitive VL flop and latch modules.

Modules that are too difficult to process and will end up having fatal warnings added.

Definitions and Theorems

Function: vl-design-always-backend-fn

(defun vl-design-always-backend-fn (x careful-p vecp)
  (declare (xargs :guard (and (vl-design-p x)
                              (booleanp careful-p))))
  (let ((__function__ 'vl-design-always-backend))
    (declare (ignorable __function__))
    (b* ((x (xf-cwtime (vl-design-caseelim x)))
         (x (xf-cwtime (vl-design-eliminitial x)))
         (x (xf-cwtime (vl-design-combinational-elim x)))
         (x (xf-cwtime (vl-design-edgesplit x)))
         (x (xf-cwtime (vl-design-edgesynth x :vecp vecp)))
         (x (xf-cwtime (vl-design-unelse x)))
         (x (xf-cwtime (vl-design-ifmerge x)))
         (x (xf-cwtime (vl-design-latchsynth x
                                             :careful-p careful-p
                                             :vecp vecp)))
         (x (xf-cwtime (vl-design-elimalways x))))
      x)))

Theorem: vl-design-p-of-vl-design-always-backend

(defthm vl-design-p-of-vl-design-always-backend
  (b* ((new-x (vl-design-always-backend-fn x careful-p vecp)))
    (vl-design-p new-x))
  :rule-classes :rewrite)