Is there an algorithm to detect race conditions in logic circuits?

Question

I'm writing a logic gate simulator. I would like to prevent user from constructing circuits prone to race condition such as flip-flops, and instead provide them as separate building blocks. Is that possible?

edit: I've got an idea. I guess that race conditions can only arise from logic circuit outputs directly or indirectly affecting their own inputs. So one way to check their validity would be to compare the truth tables of their inputs and outputs.

example one: NOT gate feeding itself

    A = !A
A | A   A | !A
--+--  ---+---
T | T   T | F
F | F   F | T
the truth tables do not match!

example two: SR NOR latch

!(A || B) = C
!(C || D) = B
!((!(A || B)) || D) = B // C => !(A || B)

 A | B | D | !((!(A || B)) || D)           B | B
---+---+---+--------------------          ---+---
 F | F | F |          F                    F | F
 F | F | T |          F                    F | F
 F | T | F |          T                    T | T
 F | T | T |          F (wrong!)           T | T
 T | F | F |          T (wrong!)           F | F
 T | F | T |          F                    F | F
 T | T | F |          T                    T | T
 T | T | T |          F (wrong!)           T | T

I hope you understand what I'm trying to convey. However, I have nothing to back it up, and I struggle to define it into an algorithm, and even if I could, it would have horrible complexity. I will try to refine it tommorow.

online truth table generator tool I used

edit 2: this is what I found in logisim manual:

Logisim will not attempt to detect sequential circuits: If you tell it to analyze a sequential circuit, it will still create a truth table and corresponding Boolean expressions, although these will not accurately summarize the circuit behavior. (In fact, detecting sequential circuits is provably impossible, as it would amount to solving the Halting Problem. Of course, you might hope that Logisim would make at least some attempt - perhaps look for flip-flops or cycles in the wires - but it does not.) As a result, the Combinational Analysis system should not be used indiscriminately: Only use it when you are indeed sure that the circuit you are analyzing is indeed combinational!

However, the amount of inputs and outputs here is finite and well defined, as opposed to infinite memory and time resources in the Halting Problem, so I do not agree that this problem is equivalent to the Halting Problem.

Answer 1

However, the amount of inputs and outputs here is finite and well defined, as opposed to infinite memory and time resources in the Halting Problem, so I do not agree that this problem is equivalent to the Halting Problem.

There are two different problems here. The simple solution (the one you should implement, in my opinion) is to simply look at the connection graph of the gates, and detect if the graph contains any cycles. If yes, simply reject the input.

The problem logisim refers to, which would amount to solving the halting problem, is one where you allow cycles, but reject sequential circuits.

This is different, because not every cycle in the graph affects the output, or worse, it affects the output but not in an sequential way.

However, the amount of inputs and outputs here is finite and well defined, as opposed to infinite memory and time resources in the Halting Problem, so I do not agree that this problem is equivalent to the Halting Problem.

Initially I disagreed, but after some more thinking, I agree. Do note that we have infinite time here - we can supply infinite sequences of inputs to the circuit in an attempt to get sequential behavior.

Under the condition that we always let a circuit stabilize before changing the inputs (or rejecting the circuit as sequential in case it never stabilizes), a finite circuit is a finite state machine. The crux is that the output of the circuit depends on the input plus the internal state of every gate in the circuit.

To prove that a circuit is non-sequential you can use the following algorithm:

1. Add the all-zero internal state to a queue.

2. While the queue is not empty, pop an internal state from the queue and construct the truth table for all inputs using that initial internal state. Also add the internal state to some set tracking internal states we have handled. For each internal state reached from this internal state while computing the truth table, add it to the queue if it's not inside our handled set.

3. If at any point in 2 a circuit does not stabilize, return sequential. If at any point during 2 the generated truth table does not equate the one from the all-zero internal state, return sequential. Otherwise return non-sequential.

Since there are a finite amount of possible internal states, this algorithm always terminates. And it fully explores all reachable states. Nevertheless, this algorithm is very, very much infeasible.