Darius Kazemi wrote a pretty thorough look at the logic behind Spelunky’s level generation. It covers the generation of the solution path (which guarantees that the level is completable), the room layouts, and how its templates work. Very informative!

http://tinysubversions.com/spelunkyGen/