[SeaBIOS] From 16 bit to 32bit