What formal mathematical models exist for digital hardware?
I am familiar with several non-formal models that are used as the basis of several hardware description language simulators and synthesizers. However, I'm not aware of any formal mathematical models, which I think would be greatly advantageous.
For an example of what I'm looking for, note that in computer science, there are several formal mathematical models of computation, such as the Lambda Calculus and the $\pi$-Calculus (http://en.wikipedia.org/wiki/Pi_calculus). There are several others that I have read about but am less familiar with.
I have found several papers talking about applying calculi to hardware description languages. For example, this one: A Calculus for Hardware Description Languages. However, most of these seem either are light on the details (like the previous example), or are attempting to provide models for specific existing hardware description languages instead of general digital hardware design.
EDIT: Here are more examples that I have found that are along the right lines, but each only model a subset of the digital hardware domain.
- Functional Netlists -- I like this a lot, but it's very focused on structure and seems to rely on pre-existing hardware primitives (maybe that's okay ...)
- Towards an Algebraic Theory of Boolean Circuits -- applicable to combinatorial digital hardware, but doesn't touch the time-domain at all
You may want to take a look at Petri Nets. It is a formal modeling language for distributed systems. It supports simultaneous processes and state at the discrete time step level. Only thing it doesn't support is signals in the hardware sense of wave signals, but it does support signals in the software sense of raising an event.