A native process algebra for VHDL

A “native” process algebra for the behavioural component of VHDL is set out without reference to another language or theory. The aim is to reduce the complexity of process algebra-based approaches to the formal verification or synthesis of hardware designs in VHDL. Recent work on the formal semantics of VHDL has allowed translation to a foreign paradigm to be avoided. The subset of the language covered excludes delta delayed signal assignments and compound signals but includes wait statements, positively delayed signal assignments and the procedural constructs