		Search-engine friendly clone of the ACL2 documentation.

Propagate

Too-hard-to-propagate

Identify wires that are too hard to propagate.

Signature
(too-hard-to-propagate x) → names
Arguments: x — Guard (vl-module-p x).
Returns: names — Type (string-listp names), given the guard.

To keep propagation simple, we don't want to try to propagate an assignment to a wire that is ever selected from. The goal is to avoid having to deal with things like this:

assign foo = a + b;
assign bar = foo[2] + 3;

Naive propagation of foo would result in:

assign bar = (a + b)[2] + 3;

And we don't want to try to think about how to handle this. Even if we just had something like assign foo = bar, it'd be complicated because foo/bar could have different ranges, e.g., if we have

wire [3:0] foo;
wire [4:1] bar;
assign foo = bar;
assign baz = foo[2] + 3;

Then we would need to be careful to fix up the indicides when substituting into baz, i.e., the correct substitution would be:

assign baz = bar[3] + 3;

And that's getting tricky. So, the basic idea is: if the wire is ever selected from anywhere, then just don't try to propagate it.

Also, for propagation to be safe, we need to make sure that we are not propagating wires that have multiple drivers. For instance, if we had:

assign A = B;
assign A = C;

Then it wouldn't be safe to just go around replacing uses of A with either B or C, because neither B nor C captures the whole value being assigned to A. Hence, we need some code for detecting what wires are driven.

Another new restriction: we now allow ourselves to propagate into modules that have always blocks, initial blocks, and function declarations. But to hopefully make this safe, we consider any names that are actually used in these places to be unsafe.

Definitions and Theorems

Function: too-hard-to-propagate

(defun too-hard-to-propagate (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'too-hard-to-propagate))
  (declare (ignorable __function__))
  (b* (((vl-module x) x))
   (mergesort
    (append
        (vl-portdecllist->names x.portdecls)
        (vl-maybe-driven-by-modinsts x.modinsts)
        (vl-maybe-driven-by-gateinsts x.gateinsts)
        (duplicated-members (vl-driven-by-assigns x.assigns))
        (used-in-some-select-p x)
        (vl-exprlist-names (vl-fundecllist-allexprs x.fundecls))
        (vl-exprlist-names (vl-alwayslist-allexprs x.alwayses))
        (vl-exprlist-names (vl-initiallist-allexprs x.initials))
        (vl-exprlist-names (vl-taskdecllist-allexprs x.taskdecls))
        (vl-exprlist-names (vl-paramdecllist-allexprs x.paramdecls))
        (vl-taskdecllist->names x.taskdecls)
        (vl-paramdecllist->names x.paramdecls))))))

Theorem: string-listp-of-too-hard-to-propagate

(defthm string-listp-of-too-hard-to-propagate
  (implies (and (force (vl-module-p x)))
           (b* ((names (too-hard-to-propagate x)))
             (string-listp names)))
  :rule-classes :rewrite)

Subtopics

Used-in-some-select-p