# Does Rice's theorem apply to sequential logic circuits?

I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any property of this circuit? I'm thinking yes, because the number of latches is bounded, so is the number of states. Even if the input is unbounded, at some point you have to arrive at a state that you've already seen before.

What are the limits of model-checking sequential circuits?

• Isn't Rice's theorem that for every non-trivial property of a program, there cannot be a verification algorithm that checks if a given program has this property? The quantification appear to be mixed up in this question. Of course, give a finite sequential circuit, there can be an algorithm (possibly depending on the circuit) that for any property of the circuit checks whether the fixed circuit has this property - it will be the "Always false" or "Always True" algorithm. Nov 17 '20 at 13:30
• I think that you want to ask the question: Is there a combination of fixed non-trivial property and algorithm, such that the algorithm can check if every execution of a sequential circuit that is input to the algorithm satisfies the property. Here, the question is yes, because a sequential circuit can be translated to a finite-state machine, and if the property that you start with is representable as a finite-state automaton, you can build the product between the machine and the automaton and check it for emptiness or universality. Nov 17 '20 at 13:32
• Having said this, there are some properties that cannot be checked by an algorithm - for instance if the output of the circuit is a possible accepting run (only the states) of a Turing machine given as initial input to the circuit. If the circuit accepts additional input and then forwards this as output, solving this problem means solving the halting problem. Nov 17 '20 at 13:33