Abort on `block :scope wire x = y;`

[whitequark]

MCVE:

module foo(input clk, a, b);
  always @(posedge clk)
    if (a) begin :scope
      wire b_inv = ~b;
    end
endmodule

 Yosys 0.8+106 (git sha1 b91debaf, clang 7.0.1-1 -fPIC -Os)

-- Parsing `test.sv' using frontend `verilog -sv' --

1. Executing Verilog-2005 frontend.
Parsing SystemVerilog input from `test.sv' to AST representation.
Generating RTLIL representation for module `\foo'.
ERROR: Abort in frontends/ast/genrtlil.cc:563.

I'm not sure how to fix it myself as I only barely know Verilog/SystemVerilog semantics. This came up while trying to write a formal testbench:

                OPCODE_ARITH: begin
                    if (i_type2 == OPTYPE_CMP) begin : scope
                        wire [15:0] tmp;
                        tmp = mem[a_regY] - mem[a_regX];
                        assert (fi_z == (tmp == 0));
                        assert (fi_s == tmp[15]);
                        // TODO: fi_c
                        // TODO: fi_v
                    end
                end

[udif]

Why are you using a wire?

I've tried your MCVE and with a few modifications, it works (Yosys 0.8+23 (git sha1 db67695, gcc 8.2.0 -fPIC -Os)

module foo(input clk, a, b);
  always @(posedge clk)
    if (a) begin :scope
      reg b_inv;
      b_inv = ~b;
    end
endmodule

[whitequark]

Why are you using a wire?

Why not?

I've tried your MCVE and with a few modifications, it works (Yosys 0.8+23 (git sha1 db67695, gcc 8.2.0 -fPIC -Os)

Yes. I know how to work around this. It's still a bug because (at least) Yosys aborts.

[daveshah1]

For reference, Vivado gives the following much nicer error:

ERROR: [Synth 8-2715] syntax error near wire 
ERROR: [Synth 8-1031] b_inv is not declared

[udif]

Why not?

Because wires are only driven by an assign statements, which are continuous. Anything driven inside an always or initial block needs to be a reg (or integer, which is a 2-value 32 bit wide reg).

In SystemVerilog you can simply use the 'logic' type for both.

[whitequark]

Thanks, I see now that the following case gives a different error:

module foo(input clk, a, b);
  always @(posedge clk)
    if (a) begin :scope
      reg b_inv = ~b;
    end
endmodule

-- Parsing `t.sv' using frontend `verilog -sv' --

1. Executing Verilog-2005 frontend.
Parsing SystemVerilog input from `t.sv' to AST representation.
Generating RTLIL representation for module `\foo'.
t.sv:4: ERROR: Invalid nesting of always blocks and/or initializations.

Although I'm not sure why, exactly, it is illegal to assign a reg like that...

[udif]

Why do you keep driving wires in an always block? This is illegal.

[whitequark]

@udif Sorry, that was a mispaste. See the updated comment.

[udif]

@whitequark , I'm not a Verilog lawyer, so I can't comment (at least yet) on the legality of initializing regs on declaration. I can certainly tell you this is not a common coding style (but then again 99.9% of my code is synthesizable, while you say this is part of a formal testbench, and assuming there are many more case items like that, using a restricted scope seems like a reasonable solution).

In my original response above I separated the declaration from the assignment, and that seemd to work.

Yosys 0.8+23 (git sha1 db67695, gcc 8.2.0 -fPIC -Os)

yosys> read_verilog /home/udif/a.v
1. Executing Verilog-2005 frontend.
Parsing Verilog input from `/home/udif/a.v' to AST representation.
Generating RTLIL representation for module `\foo'.
Successfully finished Verilog frontend.

I briefly went over the SV-2017 BNF and from the little time I've spent on this, I think assignment is only supported for wire declarations, not reg declarations.

If we go back to your original message with the formal testbench snippet, changing the wire to reg there should solve your original issue.

[whitequark]

@udif Thanks for investigation! So, the only change required here is to make Yosys print a nicer message than abort. I guess I'll implement that when I have some free time.