read_verilog doesn't respect `signed` keyword

Version

Yosys 0.39+165

On which OS did this happen?

Linux

Reproduction Steps

Consider the following code. When the input is wire0 = 6'b111101, it is a negative number less than forvar14. Therefore, reg16 takes the value of $unsigned((-forvar9)), which is -0, and the output y is 0. However, when using Yosys synthesis, the output result is 1.

module top  (y, clk, wire0);
  output wire y;
  input wire clk;

  input wire signed [5:0] wire0;

  reg reg16 = (1'h0);

  reg signed [2:0]forvar14 = (1'h0);

  reg [2:0] forvar10 = (1'h0);
  reg [2:0] forvar9 = (1'h0);

  assign y = reg16;
  always
    @(posedge clk) begin
       for (forvar14 = (1'h0); (forvar14 < (1'h1)); forvar14 = (forvar14 + (1'h1)))
        begin
       reg16 = ($signed((wire0 <= forvar14)) ? $unsigned((-forvar9)) : (^~$signed(forvar10)));
       end
    end
endmodule

testbench

`include "syn_yosys.v"

`timescale 1ns / 1ps

module testbench;

  reg clk;
  reg signed [5:0] wire0;
  wire y;

  top uut (
    .y(y),
    .clk(clk),
    .wire0(wire0)
  );

  initial begin

    clk = 0;
    wire0 = 6'b111101; 

    forever #5 clk = ~clk;
  end

  initial begin

    #100;
    $display("y = %d", y);
    $finish;
  end

  initial
    begin
      $dumpfile("wave_yosys.vcd");
      $dumpvars(0, testbench);
    end
endmodule

Here is the directory structure of the attachment. The syn_yosys.v file is the synthesized file.

In the identity directory, execute the following commands:

iverilog -o identity_main identity_testbench.v > icarus_stderr.log 2>&1
vvp -n identity_main -lxt2 > vvp_identity.log

In the syn_yosys directory, execute the following commands:

iverilog -o yosys_main yosys_testbench.v > icarus_stderr.log 2>&1
vvp -n yosys_main -lxt2 > vvp_yosys.log

to reproduce the issue. yosys_5_18.zip

📂 identity
  ├── 📄 icarus_stderr.log
  ├── 📄 rtl.v
  ├── 📄 identity_testbench.v
  ├── 📄 identity_main
  ├── 📄 vvp_identity.log

📂 syn_yosys
  ├── 📄 rtl.v
  ├── 📄 yosys_testbench.v
  ├── 📄 syn_yosys.v
  ├── 📄 icarus_stderr.log
  ├── 📄 yosys_main
  ├── 📄 vvp_yosys.log
  ├── 📄 wave_yosys.vcd

Expected Behavior

Consistent with the pre synthesis simulation, the result output is 0

Actual Behavior

Inconsistent output before and after synthesis

Actually I believe the problem is that the output verilog drops the signed from wire0, which you can confirm by testing with wire0 = 6'b0 in the testbench. The output value is actually being assigned to ^~$signed(forvar10), which is where the 1 comes from, not the negative 0.

Compare:

assign _01_ = { 1'h0, wire0[4:0] } <= (* src = "docs/test.v:19.25-19.44" *) { wire0[5], 5'h00 };

from the verific front end with the read_verilog:

assign _06_ = wire0 <= (* src = "docs/test.v:19.26-19.43" *) 3'h0;

Actually I believe the problem is that the output verilog drops the signed from wire0, which you can confirm by testing with wire0 = 6'b0 in the testbench. The output value is actually being assigned to ^~$signed(forvar10), which is where the 1 comes from, not the negative 0.

Compare:
assign _01_ = { 1'h0, wire0[4:0] } <= (* src = "docs/test.v:19.25-19.44" *) { wire0[5], 5'h00 };
from the verific front end with the read_verilog:
assign _06_ = wire0 <= (* src = "docs/test.v:19.26-19.43" *) 3'h0;

You are correct. I tried the testbench with wire0 = 6'b0, and the result was correct, which is the value 0 from $unsigned((-forvar9)). However, when I tried the following code with ($signed(wire0), the comparison was still incorrect with wire0 = 6'b111101. The actual output was the value 1 from ^~$signed(forvar10).

module top  (y, clk, wire0);
  output wire y;
  input wire clk;

  input wire signed [5:0] wire0;

  reg reg16 = (1'h0);

  reg signed [2:0]forvar14 = (1'h0);

  reg [2:0] forvar10 = (1'h0);
  reg [2:0] forvar9 = (1'h0);

  assign y = reg16;
  always
    @(posedge clk) begin
       for (forvar14 = (1'h0); (forvar14 < (1'h1)); forvar14 = (forvar14 + (1'h1)))
        begin
       reg16 = ($signed($signed(wire0) <= forvar14) ? $unsigned((-forvar9)) : (^~$signed(forvar10)));
       end
    end
endmodule

YosysHQ / yosys