The algebra of system design: A Petri net model of modular composition

A mathematically-based CAD system is being designed. The system will have a predicate logic theorem prover at its core, and will mirror every surface-level design step with an internal proof-step. Verification proofs will be byproducts of the design process: that is, circuits designed in this system will already be proven to be correct implementations of their specifications. However, an insistence that everything be expressed in pure predicate logic is as frequently obfuscating as it is clarifying: some aspects of circuit requirements and design descriptions cannot easily be expressed in logic. Allowing different expressions to infiltrate the proof-based CAD environment could destroy the mathematical integrity of the system. To protect the system while allowing more flexible descriptions, different models were used for expressing and reasoning about different requirements. The framework for the safe integration of these various models is a general-purpose composition algebra. The authors impart some of the flavor of the algebra by describing the mathematics; presenting a simple gate-level example; and, principally, by working through a relatively substantial Petri Net example. The Petri net example demonstrates that some important aspects of hardware specification and design that can only be expressed with great difficulty in other formal models of concurrency can be expressed almost effortlessly in the algebra