A theory of combinational programs

The actual behaviour of a hardware device available for an implementation of a control system can be simulated by a program, allowing the hardware device to be proved correct by standard software techniques. In this paper we formalise event semantics of hardware description language in the form of relations and use relation calculus to prove properties (including termination, stability, and uniqueness of final state) of combinational programs, the cycle behaviour of which is defined as a conditional loop of non-deterministic choices between generalised parallel assignments.