unit_t in ext_fn_t input generates invalid verliog

[blaxill]

Perhaps not conventional usage but currently unit_t/bits_t 0 sized input from an external function generates invalid Verilog. e.g.

    Definition Sigma (fn: ext_fn_t) :=
      match fn with
      | f1 => {$ unit_t ~> bits_t 32 $}
      | f2 => {$ unit_t ~> bits_t 1 $}
      end.

Generated verilog with efr_internal := false:

  // -*- mode: verilog -*-
  // Generated by cuttlec from a Kôika module
  module simple_device(input wire[0:0] CLK, input wire[0:0] RST_N, output wire[-1:0] f1_arg, output wire[-1:0] f2_arg, input wire[31:0] f1_out, input wire[0:0] f2_out);
   reg[31:0] total /* verilator public */ = 32'b0;

   assign f2_arg = 0'b0;
   assign f1_arg = 0'b0;

   always @(posedge CLK) begin
    if (!RST_N) begin
     total <= 32'b0;
    end else begin
     total <= ~f2_out && ~f2_out ? f1_out + total : (f2_out ? 32'b0 : total);
    end
   end
  endmodule

Note the output wire[-1:0] f1_arg output wire[-1:0] f2_arg and also assign f1_arg = 0'b0; assign 21_arg = 0'b0; are invalid as constants cannot be zero length (IEEE 1800-2012 - 5.7 Numbers).

Generated verilog with efr_internal := true:

// -*- mode: verilog -*-
// Generated by cuttlec from a Kôika module
module simple_device(input wire[0:0] CLK, input wire[0:0] RST_N);
  reg[31:0] total /* verilator public */ = 32'b0;

  wire[0:0] mod_f20_out;
  f2 mod_f20(.CLK(CLK), .RST_N(RST_N), .arg(0'b0), .out(mod_f20_out));
  wire[31:0] mod_f10_out;
  f1 mod_f10(.CLK(CLK), .RST_N(RST_N), .arg(0'b0), .out(mod_f10_out));

  always @(posedge CLK) begin
    if (!RST_N) begin
      total <= 32'b0;
    end else begin
      total <= ~mod_f20_out && ~mod_f20_out ? mod_f10_out + total : (mod_f20_out ? 32'b0 : total);
    end
  end
endmodule

Note .arg(0'b0) again is a zero sized constant.

[cpitclaudel]

Yeah, the unit_t type is poorly supported both in Cuttlesim and in the verilog pretty-printer, mostly because it's not always OK to eliminate the corresponding expressions (since they might have side-effects, even though they "shouldn't").

I usually solve this case-by-case. Eliminating unit arguments would be relatively easy, but what's the right way to deal with unit_t returns? (Maybe that's actually not an issue because unit_t returns will be dropped by the optimizer anyway)

I'm not sure I'll have time to look into fixing this soon; is it acceptable in your case to add a non-zero bits argument? (You typically need one to pass an enable signal to the function)

[blaxill]

I'm not sure I'll have time to look into fixing this soon; is it acceptable in your case to add a non-zero bits argument? (You typically need one to pass an enable signal to the function)

Yes thats fine, its not a pressing issue for me, I thought I'd just report it for tracking purposes.

I usually solve this case-by-case. Eliminating unit arguments would be relatively easy, but what's the right way to deal with unit_t returns? (Maybe that's actually not an issue because unit_t returns will be dropped by the optimizer anyway)

Eliding the unit_ts when generating verilog might be preferable, but I'll have a better idea after I become more familiar with Koika/how I should be using Koika (e.g. I might be trying to incorrectly shoehorn my requirements into external functions like #12 )

[blaxill]

Additionally sext can cause zero sized constants (0'b0) when extending a single bit variable, e.g. sext(a > b, 32). I think this is due to the log2 at

koika/coq/CircuitGeneration.v

Lines 113 to 117 in 61c3587

	| SExt sz width => fun a c =>
	ltac:(subst cRet; simpl; rewrite <- vect_extend_end_cast, <- (Nat.mul_1_r (width - sz));
	exact (CBinopOpt (Concat _ _)
	(CUnopOpt (Repeat 1 (width - sz))
	(CBinopOpt (Sel sz) a (CConst (Bits.of_nat (log2 sz) (pred sz)))))

Probably not caught before as this isn't required for zero extension.

FWIW, yosys doesn't accept the zero sized version 0'b0 but is fine with a plain integer 0, I think this is in line with the standard.

[cpitclaudel]

Additionally sext can cause zero sized constants (0'b0) when extending a single bit variable, e.g. sext(a > b, 32).

Thanks, I'll investigate this.

FWIW, yosys doesn't accept the zero sized version 0'b0 but is fine with a plain integer 0, I think this is in line with the standard.

Isn't that because a plain 0 is really a 32-bits 0? Would it behave correctly in a concat, for example?

[blaxill]

Isn't that because a plain 0 is really a 32-bits 0? Would it behave correctly in a concat, for example?

I believe that is correct - the official specification says it is to be a signed value of at least 32 bits. It would only be a valid substitution in some cases such as constant indexing.

[cpitclaudel]

Thanks, I'll investigate this.

Ah, yes, this is due to selection into single-bit variables begin a no-op; good catch.

[cpitclaudel]

Thanks, I'll investigate this.

Ah, yes, this is due to selection into single-bit variables begin a no-op; good catch.

This part should be fixed, at least in simple cases; can you check? (Of course, a sign extension on a one bit word is just a repeat, so it would work to use that, too)

[blaxill]

Yes it looks fixed for me thanks.