A Logic for Digital Circuits To put it simply, what i'm looking for is a logic that models sequential circuits. 
If i understood correctly, digital circuits are often categorized in two distinct categories, combinatorial and sequential, the former being a subset of the latter. Combinatorial circuits are modeled by propositional calculus, though instead of focusing on separate formulas, like propositional calculus does, it builds bigger and bigger circuits through composition of smaller ones.
More precisely, in combinatorial circuits, we are used to basically defining a set of free signals, say, A, B and C for example, and then building more complex circuits based on them, like $P = AB$, $Q = A+C$, $S = (PQ)'$ (for the less versed in boolean algebra, simply note that there's an equivalence between these operators and the usual from propositional calculus).
This simplistic approach breaks down if applied to sequential circuits. Consider our free signals R and S. One definition of a flip-flop goes like this: $Q = (R + Q_i)'$ and $Q_i = (S + Q)'$ (where "$+$" is the logical "or", and "$'$" is the logical negation). If you perform a substitution you'll see a self-reference, something propositional calculus isn't equipped to work with.
The usual explanation here is to consider prior values to $Q$ and $Q_i$. The idea here is that, if $Q$ is the logical opposite of $Q_i$, and it never so happens that we set both $R$ and $S$ to 1 (in propositional calculus parlance, $R$ and $S$ both interpreted as true), then $Q$ and $Q_i$ will always be logical opposites. From there we note that setting $R$ and $S$ both to 0 mantains the current values of $Q$ and $Q_i$, while setting only one of $R$ or $S$ to 1 sets $Q_i$ or $Q$ to 1, respectively.
I believe these are some of the topics i think answers to this question could shed some light on:


*

*What exactly do you need to add to propositional calculus in order for it to model sequential circuits? For example, sequential circuits have to do with the notion of state, which in turn basically means that the result of setting a couple of signals can vary through time - does this means we'll have to add something to model the notion of time?

*What kind of sequential circuits can we build, anyway?

*I vaguely recall that an in-depth explanations on the subject would have to explain how delay actually works in real life circuits. Indeed, real world circuits sometimes make use of a construct called buffer; in propositional calculus terms, this is simply the unary identity function! Does this factor in our logic? How so?

*Can we compose it further with other known logics?

*I've tried to look up the answer at Wikipedia and stumbled upon an approach based on Sequentions and Venjunctions - two things which not only i had never heard about before, i also failed to find any sort of useful information about. Are these concepts really related to this problem?

 A: Modern practice is to prefer designs where there are a relatively small number of "clock domains". A clock domain is a collection of sequential logic which is all clocked by the same clock net. Your example of an R-S latch suggests the more general problem.
Within a given clock domain, one has a state machine. The state can be thought of as a vector whose value changes at each clock, and whose next value depends on the previous (plus external inputs). Within this restriction it seems it's be possible to define a logic system. When sending a signal from one clock domain to another, one uses "clock domain crossing" techniques.
The primary advantage of clock domains is that they simplify the modeling, debugging, etc., of the system.

In general, one can imagine logic without the above restriction. I think this is a great topic for mathematicians to look into. Here's an example:
In order for a collection of sequential logic circuits to operate predictably, it is sufficient that there be no violation of "setup" or "hold" conditions. This is known as "static timing analysis." A "setup" condition is the requirement that incoming signals to a register be valid a certain time before the clock signal. A "hold" condition is the requirement that the incoming signal not change until after a certain time after the clock signal.
For a single clock domain, setup and hold times are easy to compute. One finds the longest (in terms of electronic delay) path from an output of the state machine to an input. This path must be short enough that signals can traverse it inside of a single clock, and still meet the setup time. This restriction gives the maximum clock frequency the clock domain can be executed at. Similarly, the shortest path must be long enough to meet the hold time. If this restriction is violated, the circuit may have errors at any frequency.
In the case of an R-S latch, the setup and hold restrictions are that one cannot turn the set and reset inputs both off at the same time. There would be a "race condition" to determine what state the latch was left in.
The above setup and hold conditions are "unilateral" (my word, there's probably a better one) in that they deal with a single signal path at a time. In fact, there is a second path that the presence of a clock domain hides from view: the delay between the clock of the driver for the source of the path and the clock for the device at the termination of the path. For a single clock domain, this is called "clock skew", but the problem generalizes in a general sequential logic system. Thus setup and hold times are "bilateral" restrictions on a circuit which consists of a loop.
Thus to ensure that a general sequential logic system meets all setup and hold times, instead of analyzing all paths, one must analyze all loops. Each such loop has two sides, a data path and a clock path. One must ensure that the "the slowest possible data path and fastest possible clock path (setup violation)" will give the same logical result as "the fastest possible data path combined with the slowest possible clock path (hold violation)." If this is so, then there can be no setup or hold violations due to that loop.
There is an analogy to this already in the mathematics literature as "network flow analysis." In this theory, one has a network with minimum and maximum flows defined on each segment. The question is whether the whole system is consistent. See "Network Flows and Monotonic Optimization" by Rockafeller for the algorithm. The difference is that in Rockafellar, the requirement is that flow be between the minimum and maximum for each path. In sequential logic, the requirement is that time delays be outside of the minimum (to avoid setup violation) or the maximum (to avoid hold violation).
