260 Chapter 14 The Facet Algebra
There are numerous mechanisms for writing this adder, including using two full
adders rather than creating a half-adder. This mechanism is a perfectly reasonable
14.5 Higher-Order Facets
Higher-order facets are facets having facet type parameters, in the same spir it as
higher-orderfunctionshaving functiontype parameters.Suchfacetsareexception-
An exceptionally common structural architecture is sequential ordering of
two or more operations. We will refer to this as the batch sequential architecture
facet batchSequential[T0,T1,T2::type]
(f1(x::T0; y::T1)::state_based;
f2(y::T1; z::T2)::state_based;
i::input T0; o::output T2)::state_based is
c1: f1(i,x);
c2: f2(x,o);
end facet batchSequential;
The batchSequential facet signature defines three universally quantified
parameters, two facet types and an input and output. The universally quantified
T0, T1, and T2 define the input, exchange, and output types associ-
ated with the facet. These types are not restricted in any way and can take any
type value desired. Making them universally quantified allows discovery or direct
specification of the desired type.
The two sequentially connected components are
f1 and f2.Facetf1 takes
component input, performs a transformation, and generates output for
f2 takes output from f1 and generates component output. The universally quan-
tified parameters must be instantiated to satisfy t ype conditions.
Now that we have a batch sequential architecture, we can put it to work
Using the Batch Sequential
by instantiating it in other systems or defining new components. The partial
system, uses sequenced negate facets to implement a delay buffer. The
buffer component instantiates batchSequential with two negation operations
and specifies inputs and outputs to the new device.
facet negate(i::input bit; o::output bit)::state_based is
end facet negate;
facet system(...)::state_based is
buffer: batchSequential(negate,negate,in,out);
end facet system;
14.5 Higher-Order Facets 261
Alternatively, we define a buffer facet that can be reused throughout a system
specification. Here a new facet,
buffer, is defined by specifying its value instan-
buffer(i::input bit,o::output bit)::state_based is
The new buffer facet is defined over two parameters that serve as input and
output for the
batchSequential instantiation. The component parameters to
batchSequential are again instantiated with copies of negate .
This Page Intentionally Left Blank

Get System Level Design with Rosetta now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.