SEMANTICS OF DIGITAL NETWORKS CONTAINING INDETERMINATE MODULES

We discuss a formal model based upon dataflow, usable for high-level digital hardware design, among other things. One of our goals is to give a denotational semantics for this model, which includes indeterminate modules. Our approach is to devise composition rules based on modelling a network by the set of its possible behaviors, i. e. sequences of computational events, where each event is the appearance or consumption of a token on a data path. A sequence of such events is called a history and a set of such histories is called an archive. We give composition rules that allow us to derive an archive for a network from the archive of its constitutents. We show how causal and operational constraints on network behavior can be inferred from the specification of archives. We also present a construction which allows us to obtain the denotation of networks containing loops by a process of successive approximations.