A formal method for provably correct composition of a real--life processor out of basic components (The APE100 reverse engineering project)