> It's decidable whether two NAND circuits implement the same function

Well, sure. At least, until you have a loop that starts clocking for you, and now you've got the halting problem.