This talk presents an ACL2 proof of the termination of a routing algorithm for
a network on-chip architecture.  After a brief presentation of the routing
algorithm, I will go through my ACL2 script.  I will first present the modeling
and the proof for a fixed size system.  Then, the algorithm is extended to the
unbounded case. Finally, I will come back to the fixed system and show how to
use the general proof for this case.