gEDA: synthesizable Verilog style

[Larry Doolittle <ldoolitt-at-NOSPAMrecycle_dot_lbl_dot_gov>]

Steve and list-lurkers -

Before I hand-edit a bunch of "legacy" code, I wonder if you could
comment on the following style of Verilog coding.  Skip all the
definitions, I care about the indentation and nested begin/end for
classic FPGA synchronous logic, including global reset:

always @(posedge clk40 or negedge rstn) if (~rstn) begin
        trace1_data <= 0;
        trace2_data <= 0;
        trace3_data <= 0;
        countl <= 0;
        counth <= 0;
        address_at_pulse_end <= 0;
end else begin
        trace1_data <= trace1_sel[0] ? ddls : dals ;  // Ref or Fwd
        trace2_data <= trace2_sel[0] ? outm : dbls ;  // Out or Rfl
        trace3_data <= trace3_sel[0] ? outm : dcls ;  // Out or Cav
        countl <= (carry | ~trace_enable) ? 0 : (countl + 1'b1);
        counth <= trace_enable ? (carry ? (counth + 1'b1) : counth) : 0;
        if (trace_enable) address_at_pulse_end <= {5'b00000, trace_address};
end

Is this good form?  Is it within the bounds that Icarus is on track to
synthesize on or about v0.8?  Is "~rstn" or "!rstn" better?  Does the
"negedge rstn" make sense?  How does Icarus pick the global reset net?

Possibly related, how does Xilinx's usage of glbl.GSR relate to all of this?
See line 69 of RAMB4_S?_S?.v .  All it seems to do on Icarus with -Wall is
generate one
xilinx/RAMB4_S8_S8.v:69: warning: implicit definition of wire history2e.trace1.trace1.b0.glbl.
message per instantiation.  I know, this module is for simulation, not
synthesis.  But I'd expect the semantics to be somehow equivalent.

          - Larry