		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-stmt-clklift

Lightweight rewriting to support allow us to support right-hand, sides such as reset ? 0 : data.

Signature
(vl-edgesynth-stmt-clklift x edgetable) → new-x
Arguments: x — Guard (and (vl-stmt-p x) (vl-edgesynth-stmt-p x)).; edgetable — Guard (vl-edgetable-p edgetable).
Returns: new-x — Type (vl-edgesynth-stmt-p new-x), given the guard.

We generally want to prohibit clocks from occurring in right-hand sides, e.g., we don't want to try to support things like:

always @(posedge clk)
   q <= a + b + clk;

However, it's essentially reasonable for us to test the clocks in a ?: expression, such as:

always @(posedge clk or posedge reset)
   q <= reset ? 0 : data;

So as a special hack, we implement a very lightweight transform to try to recognize simple right-hand sides of the form:

 clk ? a : b
~clk ? a : b
!clk ? a : b

And replace them with equivalent if-then-else statements where the clocks is used in the condition. I think this works even when there are delays, since the delays affect when the update is made, not when the right hand side values are evaluated.

Theorem: return-type-of-vl-edgesynth-stmt-clklift.new-x

(defthm return-type-of-vl-edgesynth-stmt-clklift.new-x
  (implies (and (force (if (vl-stmt-p x)
                           (vl-edgesynth-stmt-p x)
                         'nil))
                (force (vl-edgetable-p edgetable)))
           (b* ((?new-x (vl-edgesynth-stmt-clklift x edgetable)))
             (vl-edgesynth-stmt-p new-x)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-edgesynth-stmtlist-clklift.new-x

(defthm return-type-of-vl-edgesynth-stmtlist-clklift.new-x
 (implies (and (force (if (vl-stmtlist-p x)
                          (vl-edgesynth-stmtlist-p x)
                        'nil))
               (force (vl-edgetable-p edgetable)))
          (b* ((?new-x (vl-edgesynth-stmtlist-clklift x edgetable)))
            (vl-edgesynth-stmtlist-p new-x)))
 :rule-classes :rewrite)

Subtopics

Vl-edgesynth-assignstmt-clklift
Vl-edgesynth-stmtlist-clklift