A theory of combinational programs

The actual behaviour of a hardware devices available for an implementation of a control system can be simulated by a program, and this allows a 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 and stability and uniqueness of final state) of combinational programs, cycle behaviours of which are defined as a conditional loop of non-deterministic choices between generalised parallel assignments.