Proceedings Eighth Asia-Pacific Software Engineering Conference
Download PDF

Abstract

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 elations 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.
Like what you’re reading?
Already a member?Sign In
Member Price
$11
Non-Member Price
$21
Add to CartSign In
Get this article FREE with a new membership!