Workspaces ---- apbd asves asvpapers bear blast caltrop cases concurrency cosi dif diva dopcenter dopresence dopsysadmin eecsx44 elab embedded embeddedadmin giotto hyinfo m2t2 mescal metropolis mica mobies msgadmin murieh mvsis nephest ransom recons robosysadmin savg sec seminar smartnets video webmaster

Next: The VIS-v Subset Up: BLIF-MV Previous: Syntax Semantics In this section we describe the semantics of BLIF-MV. The semantics is defined over flattened networks where all the .subckt constructs are substituted recursively until leaf models. Leaf models are models without any .subckt declarations. In the following, a flattened network is called a system. At every time point, the system is in some state, where each latch has a value. An initial state of the system is a state where every latch is set to an initial state declared using the .reset constructs. Notice that the system can have more than one initial state in general. At every clock tick, all the latches update their values. These values then propagate through tables until all the wires have a consistent set of values. If a latch is encountered during the propagation, i.e. an output of a table is an input of an latch, the propagation process is stopped. Note that because of nondeterminism, given a single state, there may be several consistent sets of values. The 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. The only differences are in the interpretation of nondeterministic tables and latches with multiple initial states as described in the above. Stephen Anthony Edwards Fri Nov 22 19:07:27 PST 1996

Contact

©2002-2018 U.C. Regents