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.