Testing two DFAs generate the same language by trying all strings upto a certain length Given the language

$EQ_{\mathrm{dfa}} =$ $\{\langle A, B\rangle\mid A$ and $B$ are two DFAs and $L(A) = L(B)$ $\}$

Prove that $EQ_{\mathrm{dfa}}$ is decidable by testing the two DFAs on all strings upto a certain size. Calculate a size that works.

(This is from Sipser chapter 4)

I make a directed graph as usual but if two transitions $\delta(q_1, c_1) = q_2$ and $\delta(q_1, c_2) = q_2$ then the graph I am making will just have one edge for these two characters. My idea is to walk the directed graph in a way so that every transition is traversed, but when I walk over an edge forming a cycle, I would need to traverse the edges I have previously walked through in the cycle once again. Do this for both the DFAs and choose the greater number of edges traversed. Then enumerate through all the strings of this length (from the given alphabet) and the two DFAs are equal only if they accept and reject on the same strings.

I could probably write some pseudocode, but I'm not sure if this is the correct way to approach the problem even.
It can be tested that way, provided we may use the number of states of both automata $A$ and $B$ to compute the bound.

Note that if a finite automaton $C$ has $n$ states then any state in $C$ is reachable by a string of at most $n-1$ letters, or that state is not reachable at all. Assume I want to check whether $L(C)=\Sigma^*$. If $C$ is deterministic then all reachable states must be accepting. This can be tested by checking that all strings up to length $n-1$ are in the language. 

The check $L(A)=L(B)$ can be analyzed similarly by considering the product automaton, i.e., the automaton that simulates $A$ and $B$ in parallel.

The product construction needs a little twist. Rather than accepting if both automata accept (computing the intersection) you need to see whether both automata make the same yes/no decision. Thus accept when both components are accepting or when both components are not accepting. Thus the language is $(L(A)\cap L(B))\cup (L(A)^c\cap L(B)^c)$. If that language is $\Sigma^*$ then both automata are equivalent.