|
|
|---|
|
|
|
|---|
Replace a degenerate one-input logic gate with a buffer.
(vl-degenerate-gate-to-buf x warnings) → (mv warnings new-x)
The Verilog grammar doesn't rule out the existence of degenerate, one-input logic gates. For instance, the following is syntactically legal:
and mygate (o, a);
The Verilog-2005 Standard (Section 7.2) and SystemVerilog-2012 Standard (Section 28.4) both say Versions of these six logic gates having more than two inputs shall have a natural extension..., but do not explain the behavior in the one-input case.
Testing on Verilog-XL and NCVerilog suggests that these degenerate
wire o_buf;
wire o_and;
reg a;
buf (o_buf, a);
and (o_and, a);
initial begin
$display("1-input AND:");
a = 1'b0; #10; $display("%b -> %b (ok = %b)", a, o_and, o_and === o_buf);
a = 1'b1; #10; $display("%b -> %b (ok = %b)", a, o_and, o_and === o_buf);
a = 1'bx; #10; $display("%b -> %b (ok = %b)", a, o_and, o_and === o_buf);
a = 1'bz; #10; $display("%b -> %b (ok = %b)", a, o_and, o_and === o_buf);
end
Produces, on NCVerilog and Verilog-XL, the reasonably sensible output:
1-input AND: 0 -> 0 (ok = 1) 1 -> 1 (ok = 1) x -> x (ok = 1) z -> x (ok = 1)
However, on VCS H-2013.06-SP1 it yields something that seems broken:
1-input AND: 0 -> 0 (ok = 1) 1 -> 1 (ok = x) // wtf, 1 !== 1 ??? x -> x (ok = z) // wtf, x !== x ??? z -> x (ok = 1)
We'll mimic the behavior of Verilog-XL and NCVerilog, but warn that this is a strange construct and some Verilog tools may not support it.
Function:
(defun vl-degenerate-gate-to-buf (x warnings) (declare (xargs :guard (and (vl-gateinst-p x) (vl-warninglist-p warnings)))) (declare (xargs :guard (b* (((vl-gateinst x) x)) (and (member x.type '(:vl-and :vl-or :vl-xor :vl-nand :vl-nor :vl-xnor)) (equal (len x.args) 2))))) (let ((__function__ 'vl-degenerate-gate-to-buf)) (declare (ignorable __function__)) (b* ((x (vl-gateinst-fix x)) ((vl-gateinst x) x) ((when x.range) (mv (fatal :type :vl-bad-gate :msg "~a0: expected no instance arrays; did you forget to ~ run the replicate-insts transform?" :args (list x)) x)) (outexpr (vl-plainarg->expr (first x.args))) (inexpr (vl-plainarg->expr (second x.args))) ((unless (and outexpr (equal (vl-expr->finalwidth outexpr) 1))) (mv (fatal :type :vl-bad-gate :msg "~a0: output terminal has width ~x1 but we only ~ support 1-bit outputs. The expression for the bad ~ terminal is ~a2." :args (list x (and outexpr (vl-expr->finalwidth outexpr)) outexpr)) x)) ((unless (and inexpr (equal (vl-expr->finalwidth inexpr) 1))) (mv (fatal :type :vl-bad-gate :msg "~a0: input terminal has width ~x1 but we only ~ support 1-bit inputs. The expression for the bad ~ terminal is ~a2." :args (list x (and inexpr (vl-expr->finalwidth inexpr)) inexpr)) x)) (new-type (if (member x.type '(:vl-and :vl-or :vl-xor)) :vl-buf :vl-not)) (warnings (warn :type :vl-weird-gate :msg "~a0: ~s1 gate with a single input. We treat this as a ~ ~s2 gate, matching NCVerilog and Verilog-XL. However, ~ other Verilog tools (including for instance VCS) have ~ different interpretations. If this is really what you ~ want to do, it would be safer to use a buf gate instead." :args (list x x.type new-type))) (new-x (change-vl-gateinst x :type new-type))) (mv warnings new-x))))
Theorem:
(defthm vl-warninglist-p-of-vl-degenerate-gate-to-buf.warnings (b* (((mv ?warnings ?new-x) (vl-degenerate-gate-to-buf x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinst-p-of-vl-degenerate-gate-to-buf.new-x (b* (((mv ?warnings ?new-x) (vl-degenerate-gate-to-buf x warnings))) (vl-gateinst-p new-x)) :rule-classes :rewrite)