External function incorrectly pruned if rule is otherwise uneffectful

[blaxill]

In the following example, an external function is written to but the input value is unused/dropped. The generated verilog drops the call to total_o completely (even though it is effectful as we write a value to it). I would guess the logic optimisation pass does not correctly account for external functions.

Full source example. Relevant sections:

  Definition Sigma (fn: ext_fn_t) :=
    match fn with
    | f1 => {$ bits_t 1 ~> bits_t 32 $}
    | do_zero_i => {$ bits_t 1 ~> bits_t 1 $}
    | total_o => {$ bits_t 32 ~> bits_t 1 $} (* <-- This external function *)
    end.

  Definition _write_back : uaction reg_t ext_fn_t :=
    {{ let previous_total := read0(total) in
       let drop := extcall total_o ( previous_total ) in pass
    }}.

  Definition simple_device : scheduler :=
    write_back |> ...

  Definition ext_fn_specs (fn: ext_fn_t) :=
    match fn with
    | f1 => {| efr_name := "f1"; efr_internal := true |}
    | do_zero_i => {| efr_name := "f2"; efr_internal := true |}
    | total_o => {| efr_name := "f3"; efr_internal := true |} (* <--- *)
    end.

Note no mention of the external call in generated verilog (occurs also for 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);
	reg[31:0] total /* verilator public */ = 32'b0;

	wire[0:0] mod_f20_out;
	f2 mod_f20(.CLK(CLK), .RST_N(RST_N), .arg(1'b1), .out(mod_f20_out));
	wire[31:0] mod_f10_out;
	f1 mod_f10(.CLK(CLK), .RST_N(RST_N), .arg(1'b1), .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

Adding a dummy register and writing to it with a nonconstant value generates correct verilog:

  Definition _write_back : uaction reg_t ext_fn_t :=
    {{ let previous_total := read0(total) in
       let still_dropped := extcall total_o ( previous_total ) in (* <- still dropping value *)
       write0 (dummy, previous_total)                             (* <- but preventing rule being optimised away *) 
    }}.

[cpitclaudel]

This is correct behavior, although it can be unexpected: functions are specified to be pure (they need to have a pure model), so if their return value is unused they can be eliminated.

The trick to force them to be kept is to use the return value, e.g. by writing it to a dummy register, as you noticed.

I don't understand your second example too well — what is it about the nonconstant value?

(This will be fixed when we have proper support for modules, since function calls will become observable and hence not tivially optimizable)

[blaxill]

This is correct behavior, although it can be unexpected: functions are specified to be pure (they need to have a pure model), so if their return value is unused they can be eliminated.

I might be approaching this wrong, but my problem is that my Koika design will be part of a larger design, and the larger design is not combinational. To get signals in/out of my design I have been using external functions with efr_internal := false to expose input output signals in the verilog interface - perhaps there is another way to achieve this?

I don't understand your second example too well — what is it about the nonconstant value?

I just noticed that the external call was dropped with write0 (dummy, Ob~0) but not with write0 (dummy, previous_total), (still_dropped not mentioned in either).

[cpitclaudel]

I might be approaching this wrong, but my problem is that my Koika design will be part of a larger design, and the larger design is not combinational. To get signals in/out of my design I have been using external functions with efr_internal := false to expose input output signals in the verilog interface - perhaps there is another way to achieve this?

You're doing it right, but it requires extra care because Kôika doesn't have a good story about its module system at the moment. I summarized this in #2 (comment) , and there are more details about this in #10 ; the first link in particular has a pretty detailed description of how to do this safely (the main example we have of this is the bus in the RISCV core. If you want me to look at a concrete case I'll be happy to give design-specific advice.