Synthesis of non-blocking statements

Ok, I found this clause in the Verilog 2001 spec, section "5.4.1 Determinism":

...

Nonblocking assignments shall be performed in the order the statements were executed inside begin-end block. Consider the following example:

initial begin
  a <= 0;
  a <= 1;
end

When this block is executed, there will be two events added to the nonblocking assign update queue. The previous rule requires that they be entered on the queue in source order; this rule requires that they be taken from the queue and performed in source order as well. Hence, at the end of time step 1, the variable a will be assigned 0 and then 1.

...