Verilog always block -- testing which posedge occurred

Question

I'm trying to understand an always block construct that I'm seeing a lot. This is all in the context of trying to synthesize some hardware in an FPGA, not simulation.

Sample code:

reg out;
always @(posedge clk or posedge reset) begin
   if (reset)
     out <= 0;
   else
     out <= in;
end

What if this block is triggered by a posedge on reset? In that case, we're saying that, by definition, reset is changing. How can we then test the value of reset? It would seem to me that the value of reset should be undefined at the time of it's rising edge. For example, how can we be sure that setup and hold times are observed?

Answer 1

I agree it is ugly, but it is the "Verilog way" to implement an asynchronous reset.

How can we then test the value of reset? It would seem to me that the value of reset should be undefined at the time of it's rising edge.

You don't. Don't think like if HDLs were programming languages. The synthesizer looks at this code and concludes: "Hey, this is a rising edge D-flip-flop with an asynchronous reset, active high, always enabled". Then, it gives you one.

in the context of trying to synthesize some hardware in an FPGA

It will just find the best way to implement the described behavior with the available hardware blocks (Vivado/Zynq example):

how can we be sure that setup and hold times are observed?

This is above the scope of Verilog/VHDL. Check the synthesis tool documentation to see how this can be done with constraints and timing simulations.