NoC SAT Routing

[soheilshahrouz]

This PR formulated NoC routing as a SAT problem and invoked cp-sat solver in or-tools to find a deadlock-free solution with the minimum congestion.

Description

Turn model routing algorithms used during annealing generate minimal routes between NoC routers. Congestion may not be resolved with minimal routing. If any NoC link is still congested at the end of the annealing process, we use a SAT solver to find traffic flow routes that minimize congestion while trying to meet latency constraints and prevent the aggregate bandwidth from growing too much.

Types of changes

• Bug fix (change which fixes an issue)
• New feature (change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)

Checklist:

• My change requires a change to the documentation
• I have updated the documentation accordingly
• I have added tests to cover my changes
• All new and existing tests passed

[vaughnbetz]

@soheilshahrouz : it's worth writing up how you handle the dependence on google OR tools in this PR.

• This feature is off by default
• If enabled with a Cmake variable, it searches for an installed set of OR tools. If not found, it prompts the user.
  That seems pretty safe to me.

[vaughnbetz]

Do we have a test of the SAT NoC router? Should add a test that builds it and runs it on some configuration.