Formal verification for equivalence checking between MuGrpahs

[wmdi]

Description of changes:
It is consistent with the probabilistic verifier in the gated_mlp workload.

For the attention workloads, it accepts more mugraphs than the probabilistic one. I manually checked the mugraphs and think they are correct (I might be wrong since it is not easy to check the correctness of a mugraph).

There are also performance issues:

1. The verifier currently can only check one mugraph at a time for the ease of implementation, which is a bottleneck in some workloads;
2. We can fine tune the time/resource limit of the solver to achieve the balance between solver accuracy and performance.

Related Issues:

Linked Issues:

• Issue #

Issues closed by this PR:

• Closes #

[jiazhihao]

It's surprisingly that it accepts more muGraphs than probabilistic verification. If you think these muGraphs are correct, this means there is a bug in our fingerprint calculation logic. Do you think we can look into one such example during the meeting today?

[wmdi]

Let's merge #142 first and resolve the conflict in this PR