Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

unit_t in ext_fn_t input generates invalid verliog #11

Open
blaxill opened this issue Apr 26, 2021 · 8 comments
Open

unit_t in ext_fn_t input generates invalid verliog #11

blaxill opened this issue Apr 26, 2021 · 8 comments

Comments

@blaxill
Copy link

blaxill commented Apr 26, 2021

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
Copy link
Collaborator

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
Copy link
Author

blaxill commented Apr 26, 2021

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
Copy link
Author

blaxill commented Apr 28, 2021

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

| 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
Copy link
Collaborator

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
Copy link
Author

blaxill commented Apr 28, 2021

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
Copy link
Collaborator

Thanks, I'll investigate this.

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

@cpitclaudel
Copy link
Collaborator

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
Copy link
Author

blaxill commented May 6, 2021

Yes it looks fixed for me thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants