Hardware Reference
In-Depth Information
always @($global_clock)
o<=a;
endmodule :m
This model is much simpler than that in Example 21.7 . While the simulation model
remains exactly the same, c is no longer a variable of the FV model. To understand
the transition diagram, consider the state f i g as an example. In this state, i D 1 and
o D 0. In the next tick of the system clock o must be 0, while i may assume any
value. Thus, we have two transitions: f i g!; , and f i g!f i g .
t
21.2.2
Model Language
We can interpret each state of an FV model as a letter in the alphabet ˙ D 2 V .The
notation 2 V is used to designate the set of all subsets of the set V . For instance, the
alphabet of the FV model from Example 21.8 is ˙ Df; ; f i g ; f o g ; f i; o gg . 4
According to its transition relation, the FV model accepts some sequences,
or paths , of its states, while it prohibits others. For instance, the model from
Example 21.8 accepts the sequence of states f i g ; f i g ;:::because it has the transition
f i g!f i g ”, whereas the model forbids the sequence ; ; ; ;::: because it does not
have the transition ;!; . Therefore, an FV model defines an infinitary language
(see Sect. 21.1.3 ) over ˙ consisting of all the paths it accepts. The path q 0 ;q 1 ;:::
is accepted by the FV model if it starts in an initial state: q 0 2 I , and each pair of
consecutive states q i and q i C 1 is connected by the transition relation: .q i ;q i C 1 / 2 R.
These paths are exactly the words of the model language L.M /. According to the
terminology introduced in Sect. 21.1.3 , the words are also called traces, and they are
traces as also understood by hardware engineers. Indeed, a trace may be considered
as a dump of all variable values at each tick of the global clock. The main difference
between these traces and conventional simulation traces is that the simulation traces
are finite, whereas the FV model defines infinite traces.
21.2.3
Symbolic Representation
In the above examples, we built explicit representations of FV models: each state
and each state transition appeared separately. This approach is feasible only when
the number of variables is very small. Even a modest design containing 300 state
elements (latches and flip-flops) may have more states than there are atoms in the
universe! To address this problem, a symbolic state representation is used.
4 We distinguish between the alphabet ˙ and the set of states Q since in the general Q does not
need to contain all combinations of variables, whereas ˙ does.
Search WWH ::




Custom Search