The Software Package BALM - The Unknown Component Problem: Theory and Applications - page 130

table and the inputs of the other tables. Thus a named variable is conceptually a
wire. If a table is deterministic and binary, it can also be thought of as a logic gate.
A latch is the state-holding element of BLIF-MV . It has only one input. Its output
has the same set of allowed values (domain) as its input. A set of initial values is
associated with every latch; they must be a subset of the domain of the latch. A state
is an assignment of values to the latches of a design, where a value assigned must
be in the domain of the latch. An initial state is a state where every latch takes one
value from its set of initial values. A latch can have more than one initial state in
general.
The semantics are as follows. At every time point, the system is in some state
(each latch has a value). At every clock tick, each latch updates its output value to be
its current input value. These outputs then propagate through tables in a topological
order until all the wires have a consistent set of values, i.e. each output value of a
table is one of the set of allowed values for the set of input values on the inputs
to the table. If a latch is encountered during the propagation, i.e., an output of a
table is an input to a latch, the propagation process is stopped. Note that because of
nondeterminism, given a single state in the latches, there may be several consistent
sets of values on the wires. These semantics can be seen as a simple extension of the
standard semantics of synchronous single-clocked digital circuits. In fact, if every
table is deterministic and every latch has a single initial state, the two semantics are
exactly equal. Thus, the only differences are in the interpretation of nondeterministic
tables and latches with multiple initial states.
In BALM, the command read blif mv reads a BLIF-MV (or BLIF )
description, and then sets up a corresponding internal data structure to represent the
multi-valued nondeterministic network. The write blif mv command writes a
BLIF-MV description to a file. Although the BLIF-MV format was designed as a
logic exchange format, simple examples in BLIF-MV are readable and can exhibit
some degree of clarity.
Example 8.1. We show an example of the BLIF-MV description of a multi-valued
network with one internal node and one latch, where all signals are 3-valued:
.model blif_mv_example
.inputs a
.outputs f g
.mv a,f,g 3
.table a g -> f
.default 0
101
022
.latch f g
.reset g
2
.end
For a more detailed treatment of the BLIF-MV format and some examples, see [75].