Reset Query

I believe that one of the issues of async resets (In this case async deassertion) is that is you have a large amount of clock skew throughout a large FPGA then if the reset is deasserted asynchronously very close to the clock edge then it is possible that some flip-flops will see one clock edge as the first after reset and others will see subsequent edges.

It all depends on the amoutn of clock skew in your design and clock frequency.

For example a 2 bit counter, bit 0 might be first clocked on clock edge n and Bit 1 on clock edge n+1, giving perhaps not the results you expected!

The clock skew may vary on each fit so you might see behavioural changes on each re-fit with async resets.

Hence I always go for synchronous deassertion, usually with async assertion.

So a long winded way of saying, I would use your option 2 :)