Verilator bug with signedness and arithmetic shift

[veripoolbot]

---

Author Name: Clifford Wolf (@cliffordwolf)
Original Redmine Issue: 756 from https://www.veripool.org
Original Date: 2014-05-01
Original Assignee: Wilson Snyder (@wsnyder)

---

Verilator b631b59 returns 1 instead of 0 for a=-1 and b=7:

  input signed [4:0] a;
  input [2:0] b;
  output [3:0] y;
  assign y = |0 != (a >>> b);
endmodule

Self-contained test case:

http://svn.clifford.at/handicraft/2014/verilatortest/test008.v

http://svn.clifford.at/handicraft/2014/verilatortest/test008.cc

http://svn.clifford.at/handicraft/2014/verilatortest/test008.sh

Verilog testbench for comparison:

http://svn.clifford.at/handicraft/2014/verilatortest/test008_tb.v

[veripoolbot]

---

Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2014-05-03T02:23:46Z

---

Based on another simulator, I believe your case is equivalent to:

       w4_u = (5'b0 == (5'sb11111 >>> 3'd7));  // Vlt !=, most sims ==

Everyone agrees, if comparing to signed:

       w4_u = (5'sb11111 == (5'sb11111 >>> 3'd7));  // Agreement

This implies other simulators are propagating the sign of the == down to the RHS of the
shift. I believe this is incorrect, I do not see what in IEEE says to do this.

Further experiments:

       // Does >>> normally expression-propagate the sign from the upper expression (IEEE says yes)?
       w4_u = (1'b0+(5'sb11111 >>> 3'd7));
       `checkh(w4_u, 4'b0000);  // Yes, agreement
       w4_u = (1'sb0+(5'sb11111 >>> 3'd7));
       `checkh(w4_u, 4'b1111);  // Yes, agreement

Does eq '= =' normally propagate a sign between LHS and RHS? IEEE does not say, but implies not as it talks about separation of signs on each side

       w4_u = (5'b0 == (5'sb11111 / 5'sd3));  // Must be signed result (-1/3) to make this result zero
       `checkh(w4_u, 4'b0001);   // Disagreement.  One commercial simulator says yes, another no.
       w4_u = (5'sb0 == (5'sb11111 / 5'sd3));  // Must be signed result (-1/3) to make this result zero
       `checkh(w4_u, 4'b0001);   // Agreement
       w4_u = (5'b01010 == (5'b11111 / 5'sd3));  // Sanity check unsigned has correct result
       `checkh(w4_u, 4'b0001);   // Agreement

I cannot justify why == would propagate signed to a >>> subexpression
but not for a division subexpression, as your example seems to require
or one of the commercial simulators. On the other hand, the other
commercial simulator does propagate signed, but this seems to disagree with
IEEE and that simulator messes up other testcases not shown here.

Please run the attached and check results on your other simulators.

[veripoolbot]

---

Original Redmine Comment
Author Name: Clifford Wolf (@cliffordwolf)
Original Date: 2014-05-03T11:54:32Z

---

Wilson Snyder wrote:

I cannot justify why == would propagate signed to a >>> subexpression but not for a division subexpression

In my tests the signdness is also propagated for a division subexpressions. (see 'e' and 'f' outputs in the test below)

I do not see what in IEEE says to do this.

Sec. 5.5.1 of IEEE Std 1364-2005 does. But it is subtle because you need to know that "expression" means "the whole expression". (Which is kind-of clear after the discussion of expression bit lenghts in the previous chapter and from the fact that a different interpretation of "expression" would not yield a consistent set of rules.)

Only the cases where the wording "regardless of the operands" is used are cases where "the expression" stops and the subexpression may have a different signdness.

Note that comparison results are such a case. So the result of a comparison is always unsigned. But this does not decouple the operands of the comparison operator from each other, it only decouples the result of the comparison from the comparison itself.

Please run the attached and check results on your other simulators.

I've created a testcase based on your example code:

http://svn.clifford.at/handicraft/2014/verilatortest/test009.v

http://svn.clifford.at/handicraft/2014/verilatortest/test009.cc

http://svn.clifford.at/handicraft/2014/verilatortest/test009.sh

and run it on various simulators:

0111011 -- Verilator
1101011 -- Icarus Verilog
1101011 -- Xilinx XSim
1101011 -- ModelSim
1101011 -- Yosys eval

So the differences are:

assign c = (1'b0+(5'sb11111 >>> 3'd7));    // Verilator: 1, Everyone else: 0

[veripoolbot]

---

Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2014-05-03T12:44:13Z

---

I understand how 5.5.1 applies to expressions (BTW you're better looking at 2012), but no where does it say exactly what operators are subject to this rule; some rules of thumb apply like it applies to those that are not self-determined but this sort of assumption is what half of these bugs are about.

Thanks for the data; what mostly matters to me is the big three which get heavy testing: Modelsim and NC-Verilog which agree, VCS disagrees (1101111 and the source of confusion above). I'll file a bug on VCS and go with the Modelsim answer which matches yours.

[veripoolbot]

---

Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2014-05-03T13:26:07Z

---

Ok, with the expected values now clear it was a simple change to shift.

Fixed in git towards 3.857.

[veripoolbot]

---

Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2014-05-10T12:18:13Z

---

Resolved earlier

[veripoolbot]

---

Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2014-05-11T21:11:44Z

---

In 3.860.