| |
|
|
    Next: Introduction to Formal Up: No Title Previous: Introduction to VIS
Describing Designs for VISGiven the special needs of hardware simulation, verification, and synthesis, specialized languages to describe hardware have been defined. These are called hardware description languages (HDLs) and they resemble general-purpose programming languages. Modern HDLs enable the designer to mix different levels of design abstraction.
Verilog HDLThe two most widely used languages for digital design are Verilog, based on C, and VHDL, based on ADA. Currently VIS only supports Verilog, but our intermediate format, BLIF-MV, was designed to support translation from many languages. Verilog allows mixed-level descriptions of hardware in terms of static structures and dynamic behaviors. Dynamic behavior is described by means of high-level constructs as found in general-purpose programming languages, like conditional, control of loops, and process fork-join. A specification in Verilog consists of one or more modules. The top level module specifies a closed system containing both test data and hardware models. Component modules normally have input and output ports. Events on the input ports cause changes on the outputs. Events can be either changes in the values of wire variables (i.e., combinational variables) or in the values of reg variables (i.e., register variables), or can be explicitly generated abstract events. Modules can represent pieces of hardware ranging from simple gates to complete systems (e.g., microprocessors), and they can be specified either behaviorally or structurally, or by a combination of the two. A behavioral specification defines the behavior of a module using programming language constructs. A structural specification expresses a module as a hierarchical interconnection of submodules. The components at the bottom of the hierarchy are either primitives or are specified behaviorally. Verilog has a library of predefined primitives. A good reference for Verilog can be found in [1].
VL2MV: from Verilog to BLIF-MVVIS operates on an intermediate format called BLIF-MV, which is an extension of BLIF, the intermediate format for logic synthesis accepted by SIS and other tools. VIS includes a stand-alone compiler from Verilog to BLIF-MV, called VL2MV. See [2] for a description of the synthesizable subset of Verilog that can be handled by VL2MV and of the extensions of Verilog that are also supported by VL2MV. In this section we survey the key features of Verilog for VL2MV. Conceptually, it would be easy to provide a translator from any other HDL language, like VHDL or Esterel, to BLIF-MV.
The relationship between a behavioral description language like Verilog
and a machine description language like BLIF-MV is similar to that between
a high-level programming language and an assembly language.
Basic constructs of BLIF-MV are module declarations/instantiations,
input-output relational tables which allow descriptions of nondeterminism,
symbolic wires, and latches.
In BLIF-MV, symbolic latches are implicitly controlled by a global clock.
This clock does not need to be a real wire
in the hardware sense. All symbolic latches transit instantaneously
to the next state indicated by the relevant transition tables.
At each clock cycle, each table continuously updates its outputs according
to the inputs it sees until convergence is reached.
VL2MV extracts a set of interacting finite state machines (FSMs)
that preserve the behavior of the source Verilog program defined
in terms of simulated results.
Allocation of hardware gates to operators in Verilog
(resource binding) is based on the assumption of unlimited resources,
where resources are all possible gates expressible in one table in BLIF-MV.
No scheduling and optimization are performed, so the extracted FSMs
are not guaranteed to be optimal (for area, speed, and so on).
In order to optimize the logic, a synthesis program like SIS can be
invoked on modules of the system. A design in a synthesizable subset of Verilog consists of a set of modules (either hardware or software). The first module encountered is regarded as the root module. All modules run in parallel and communicate with each other through a set of channels (set of wire variables declared in the modules to which these channels belong). It is assumed that communication through channels is instantaneous. Within each module, values on channels can be accessed through a set of ports, that can be either wires or registers. Through wire ports, a module can input and output from and to channels instantaneously, while through register ports it takes one time unit. A wire port has no storage element associated with it, while a register port has one storage element associated with it. A Verilog module contains declarations, module instantiations, continuous assignments and procedural blocks. Continuous assignments begin with the keyword assign and are always active; they can be thought of as combinational blocks. Procedural blocks are referred to as always statements; statements within a procedural block are executed sequentially. Module instances, continuous assignments, and procedural blocks within a module run concurrently. Execution of each continuous assignment, basic block in a procedural block and module instance is assumed to be atomic within each instant. If there is more than one procedural block in the same module, and outputs of one are inputs to another, the simulated result may depend on how expressions from different blocks are interleaved by the simulator. VL2MV can be invoked as a stand-alone tool on a Verilog file to produce a BLIF-MV file. This can be read in VIS with the command read_blif_mv. As an alternative, the command read_verilog can be directly used to read in a Verilog file. This invokes VL2MV internally.
Features of Verilog Supported by VL2MVVL2MV supports a synthesizable subset of Verilog, and also extends it minimally to make it usable for formal verification. We survey the features that characterize Verilog as supported by VL2MV.
AssignmentsContinuous assignments are always active, i.e., whenever any input changes, the output is updated instantaneously. Only wire variables can be used at the left hand side of continuous assignments. Continuous assignments describe the combinational behavior of a circuit. Procedural assignments (= within a procedural block), also referred to as blocking assignments, execute sequentially within a procedural block, changing the content of state variables, until the execution is blocked by a pause. VL2MV compiles procedural blocks based on the assumption that each basic block will be executed atomically if the delay/event control of the block is satisfied. VL2MV assumes also that execution of procedural assignments takes zero hardware time. All procedural blocks with active event controls get executed concurrently. Notice that a Verilog simulator does not treat simple blocks as atomic. If there is more than one procedural block sharing the same reg variables, caution should be taken to make sure that the desired behavior does not depend on a specific interleaving among processes. Procedural assignments update variables instantaneously, meaning that they change the left-hand side variable so that the statement following the assignment (in the same process, or always statement) can observe the value change. On the other hand, other processes (for instance, other always statements or continuous assignments) cannot see the change until the next clock cycle. Because of this, race conditions might arise among multiple procedural assignments. Non-blocking procedural assignments (<=) provide a mechanism that defers the assignment without blocking the execution of statements in a block. On encountering a non-blocking assignment, the right hand-side of the assignment is evaluated according to the most recent values of the referred variables. However, without changing the variable on the left hand-side, program execution continues. Then variables are updated simultaneously at the very beginning of the next time slot. For VL2MV, non-blocking procedural assignments should never be used, since they might introduce unwanted nondeterminism.
NondeterminismNon-blocking assignments also provide a way to introduce nondeterminism on reg variables. If there is more than one non-blocking assignment in the current time slot assigning to the same register variable, then the value of that register variable in the next clock cycle will be nondeterministically chosen from those assigned values. Even though VL2MV accepts this way of specifying nondeterminism, in VIS, unlike in HSIS, multiple assignments are not considered legal nondeterminism.
Instead, a nondeterministic construct, $ND, has been added to Verilog
to specify nondeterminism on wire variables and is
the only legal way to introduce nondeterminism in VIS.
For example, to require that the output at a particular state is
nondeterministically GO or NOGO, one can introduce a new variable,
assign r=$ND{GO,NOGO};
.
.
always@(posedge clk) begin
.
.
state = r;
.
.
end
Symbolic VariablesSometimes it is desirable to specify and examine the value of some variables symbolically, rather than having to explicitly encode them. VL2MV extends Verilog to allow users to declare symbolic variables using an enumerated type mechanism similar to the one available in the C programming language. As an example, we introduce a symbolic type named door:
typedef enum {OPEN,OPENING,CLOSED,CLOSING} door;
Implicit vs. Explicit ClockingThe clocking discipline is determined by the definition of the Verilog simulator, and it can be either implicit or explicit. Implicit is the default. Explicit may be required in some cases. A Verilog simulator is an event-driven passive scheduler. A simulator schedules events generated from Verilog modules and then sends them to modules which are sensitive to these events. Statements with sensitized events (active statements) are executed and in turn more events are generated, which are then scheduled by the simulator. The simulator itself does not generate any event, but it coordinates between the producers and consumers of events. Hence, to write a synchronous system, a designer needs to write a small clock generator, i.e., an event generator which creates events in time. The produced events provoke a chain of reactions among modules. The system reaches a stable state when there are no more events other than the clocking event. The next clocking event is then chosen by the simulator, and simulation time is advanced according to the time stamp of the newly scheduled clocking event. We call the system implicitly clocked when all transitions are synchronized by an implicit time. For an implicitly clocked system hardware resources will not be allocated for a synchronizing variable. Also, for implicitly clocked designs, one symbolic latch (or state variable) is allocated for each reg variable, and synchronization variables are dropped. By default, implicit clocking semantics is assumed. On the other hand, for some designs, the operation of a system depends explicitly on several phases (rising edge, falling edge, 1-level, 0-level) of one or more synchronizing signals (generally referred to as clocks). In such a case the clock signals should be interpreted literally and hardware resources should be allocated. A design is called explicitly clocked if synchronizing signals are to be compiled literally into hardware. For explicitly clocked systems, each reg variable is modeled by a symbolic latch along with some extra logic to emulate the clocking mechanism. An example of explicit clocking declared by the user is the following. Suppose that a system is composed of parallel components that progress differently according to synchronization signals exchanged among them by means of wait statements. Then it is necessary to declare an explicit clocking signal:
module env; reg clk; initial clk=0; always #1 clk = !clk; endmodule This code generates a clocking signal clk with a cycle of two time units used to drive the whole system and make it simulatable. In this case VL2MV must be invoked with the options -c -F, meaning explicit clocking (-c), and ignore all timing (-F).
Verilog for VL2MV: Hints and TrapsIn this section a list of hints to follow, and traps to avoid, is provided for writing Verilog for VIS.
BLIF-MVBLIF-MV is a low-level language designed for describing hierarchical symbolic sequential systems with nondeterminism. A system can be composed of interacting sequential subsystems, each of which can be again described as a collection of communicating sequential subsystems. This makes it possible to describe systems in a hierarchical fashion. The internal data structure of SIS does not support hierarchical representations. Hence, even though BLIF can describe hierarchy, BLIF descriptions are flattened into a single-level representation within SIS. In VIS, however, the original hierarchy specified in BLIF-MV is preserved in internal data structures so that true hierarchical synthesis and verification is possible.
BLIF-MV also allows nondeterministic gates The semantics of BLIF-MV is defined over flattened networks, using a combinational/sequential concurrency model. There are four basic primitives: variables, tables (intuitively nondeterministic gates), wires and latches. A variable takes values from some finite domain. A relation defined over a set of variables is represented using a table. The variables of a table are divided into inputs and outputs. A particular variable can be designated as an output in at most one table. Tables are inter-connected using wires. If a table is deterministic and Boolean, it may also be thought of as a logic gate. Wires may only take values in the domain of the corresponding variable. A latch is a specialized element that can be placed on a wire. The latch divides the wire into two parts; the input to the latch, and the output of the latch. A set of initial values is associated to every latch; they must be a subset of the set of values of its wire. A state is an assignment of values to the latches of a model, where a value assigned to a latch must be in its domain. An initial state is a state where every latch takes a value from its set of initial values. Note that the system can have more than one initial state in general. At every time point, the system is in some state, where each latch has a value. 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 through that latch is stopped. Note that because of nondeterminism, given a single state, there may be several consistent sets of values. This 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. In VIS the command read_blif_mv reads a BLIF-MV description created by VL2MV, or some other means, and then sets up a corresponding internal data structure. The write_blif_mv command writes a BLIF-MV description to a file. The BLIF-MV format is not meant to be read or written directly by the user, even though simple examples in BLIF-MV may exhibit some degree of clarity. In the VIS documentation, the syntax of BLIF-MV is described in the document entitled ``BLIF-MV''.
BLIFBLIF (Berkeley Logic Interchange Format) is an intermediate format to describe sequential circuits. It has been defined as an entry point to logic optimizers such as SIS, the synthesis system developed at UC Berkeley. A BLIF file represents a sequential circuit either as an interconnection of logic gates and latches or as the state transition table of a finite state machine (FSM) or in both ways (an FSM and a corresponding gate-level implementation). It is possible to have VIS and SIS interact, by sending to SIS a binary encoded and deterministic sequential circuit and receiving back an optimized version of the same. Notice that even though SIS can also handle KISS files (i.e., partially encoded and partially deterministic FSMs), currently VIS outputs hardware FSM descriptions (i.e., a netlist describing completely encoded and completely deterministic FSMs), for SIS input. For a description of BLIF and SIS we refer to the tutorial paper [4]. A BLIF description can be read directly into VIS by the command read_blif, while write_blif converts the internal VIS data structure into a BLIF file readable by SIS. The synthesis path from VIS to SIS and back and related commands are described in Chapter 5.
Nondeterminism and Incomplete Specification
The only form of nondeterminism supported in VIS is the construct
$ND in Verilog.
A system so described is considered internally as deterministic,
because pseudo-input variables are introduced to ``control'' this form
of nondeterminism.
Pseudo-input variables are, by definition, those variables introduced
by a $ND construct.
A Verilog nondeterministic assignment, like
# assign rand_choice = $NDset ( 0,1 ) .names -> rand_choice 0 1 There are other ways of introducing nondeterminism in Verilog that are supported by VL2MV and HSIS, but are not supported by VIS. VL2MV always produces completely specified BLIF-MV tables. However, a BLIF-MV file not produced by VL2MV (but by another tool or manually) may contain incomplete specification. When the internal data structure is built, each table is checked for determinism and complete specification (with the exception of the pseudo-inputs). This is a conservative test, in the sense that one or more tables may be nondeterministic while the entire network is deterministic. Similarly, one or more tables may be incompletely specified while the network is completely specified.
Example: a Traffic Light ControllerIn this tutorial, we will use the example of a traffic light controller (TLC), first introduced by Mead and Conway [5], to illustrate several concepts. A little used farm road intersects a multi-lane highway; a traffic light controls the traffic at the intersection. The light controller is implemented to maximize the time the highway light remains green. The main module ties together a timer, a sensor, a farm light control and a highway control submodules. The timer submodule implements a timer, that outputs ``short'' and "long" timeouts. The highway light stays green for at least ``long'' time. Any time after ``long'' time, if there is a car waiting on the farm road, then the farm light turns green. The farm light remains green until there are no more cars on the farm road, or until the long timer expires. The yellow light for both directions stays yellow for ``short'' time. Note that only a single timer is used for both the farm road and highway controllers. In theory, this could lead to conflicts; as implemented, such conflicts are avoided. From the START state, the timer produces the signal ``short'' after a nondeterministic amount of time. The signal ``short'' remains asserted until the timer is reset (via the signal ``start''). From the SHORT state, the timer produces the signal ``long'' after a nondeterministic amount of time. The signal ``long'' remains asserted until the timer is reset. Notice that the use of nondeterminism in the description of the timer models an infinite number of actual implementations, each with a different set-up for the ``short'' and ``long'' periods. The farm light stays RED until it is enabled by the highway control. At this point, it resets the timer, and moves to GREEN. It stays in GREEN until there are no cars, or the long timer expires. At this point, it moves to YELLOW and resets the timer. It stays in YELLOW until the short timer expires. At this point, it moves to RED and enables the highway controller. The highway light stays RED until it is enabled by the farm control. At this point, it resets the timer, and moves to GREEN. It stays in GREEN until there are cars on the farm road and the long timer expires. At this point, it moves to YELLOW and resets the timer. It stays in YELLOW until the short timer expires. At this point, it moves to RED and enables the farm controller. There is a single sensor that detects the presence of a car in either direction of the farm road. At each clock tick, it nondeterministically reports that a car is present or not. The fact that the timer is a Moore machine (while the highway and farm controllers are Mealy machines) ensures that the component FSMs can be combined to form a well-defined product FSM (without combinational cycles).
Fig. 2.1 is a block diagram for the entire controller, and Fig. 2.2 describes the four FSMs that make up the system.
This entire example is written in Verilog as:
/* Written by Tom Shiple, 25 October 1995 */
/* Symbolic variables */
typedef enum {YES, NO} boolean;
typedef enum {START, SHORT, LONG} timer_state;
typedef enum {GREEN, YELLOW, RED} color;
module main(clk);
input clk;
color wire farm_light, hwy_light;
wire start_timer, short_timer, long_timer;
boolean wire car_present;
wire enable_farm, farm_start_timer, enable_hwy, hwy_start_timer;
assign start_timer = farm_start_timer || hwy_start_timer;
timer timer(clk, start_timer, short_timer, long_timer);
sensor sensor(clk, car_present);
farm_control farm_control(clk, car_present, enable_farm, short_timer, long_timer,
farm_light, farm_start_timer, enable_hwy);
hwy_control hwy_control (clk, car_present, enable_hwy, short_timer, long_timer,
hwy_light, hwy_start_timer, enable_farm);
endmodule
module sensor(clk, car_present);
input clk;
output car_present;
wire rand_choice;
boolean reg car_present;
initial car_present = NO;
assign rand_choice = $ND(0,1);
always @(posedge clk) begin
if (rand_choice == 0)
car_present = NO;
else
car_present = YES;
end
endmodule
module timer(clk, start, short, long);
input clk;
input start;
output short;
output long;
wire rand_choice;
wire start, short, long;
timer_state reg state;
initial state = START;
assign rand_choice = $ND(0,1);
/* short could as well be assigned to be just (state == SHORT) */
assign short = ((state == SHORT) || (state == LONG));
assign long = (state == LONG);
always @(posedge clk) begin
if (start) state = START;
else
begin
case (state)
START:
if (rand_choice == 1) state = SHORT;
SHORT:
if (rand_choice == 1) state = LONG;
/* if LONG, remains LONG until start signal received */
endcase
end
end
endmodule
module farm_control(clk, car_present, enable_farm, short_timer, long_timer,
farm_light, farm_start_timer, enable_hwy);
input clk;
input car_present;
input enable_farm;
input short_timer;
input long_timer;
output farm_light;
output farm_start_timer;
output enable_hwy;
boolean wire car_present;
wire short_timer, long_timer;
wire farm_start_timer;
wire enable_hwy;
wire enable_farm;
color reg farm_light;
initial farm_light = RED;
assign farm_start_timer = (((farm_light == GREEN) && ((car_present == NO) || long_timer))
|| (farm_light == RED) && enable_farm);
assign enable_hwy = ((farm_light == YELLOW) && short_timer);
always @(posedge clk) begin
case (farm_light)
GREEN:
if ((car_present == NO) || long_timer) farm_light = YELLOW;
YELLOW:
if (short_timer) farm_light = RED;
RED:
if (enable_farm) farm_light = GREEN;
endcase
end
endmodule
module hwy_control(clk, car_present, enable_hwy, short_timer, long_timer,
hwy_light, hwy_start_timer, enable_farm);
input clk;
input car_present;
input enable_hwy;
input short_timer;
input long_timer;
output hwy_light;
output hwy_start_timer;
output enable_farm;
boolean wire car_present;
wire short_timer, long_timer;
wire hwy_start_timer;
wire enable_farm;
wire enable_hwy;
color reg hwy_light;
initial hwy_light = GREEN;
assign hwy_start_timer = (((hwy_light == GREEN) && ((car_present == YES) && long_timer))
|| (hwy_light == RED) && enable_hwy);
assign enable_farm = ((hwy_light == YELLOW) && short_timer);
always @(posedge clk) begin
case (hwy_light)
GREEN:
if ((car_present == YES) && long_timer) hwy_light = YELLOW;
YELLOW:
if (short_timer) hwy_light = RED;
RED:
if (enable_hwy) hwy_light = GREEN;
endcase
end
endmodule
Next: Introduction to Formal Up: No Title Previous: Introduction to VIS
Yuji Kukimoto Tue Feb 6 11:58:14 PST 1996 |
| Contact |
| ©2002-2018 U.C. Regents |
, and write the following Verilog fragment.
