$Id: HowToWriteVerilogForVl2mv,v 1.2 2001/05/26 22:20:04 vis Exp $ The use of vl2mv imposes several restrictions on how systems are described in Verilog. Here we discuss some of these restrictions and make a few recommendations on coding style. These notes are intended as a supplement to the existing documentation on how to code in Verilog for VIS. * CLOCKS For the sake of efficiency, use just one clock if possible. If the circuit has multiple, phase-locked clocks, consider using gating signals instead. Do not use always blocks to model combinational logic by putting the inputs in the sensitivity list. You have two options as alternatives: 1. Describe the combinational logic using "assign" statements. This implies replacing "if" statements with "cond ? expr1 : expr0" expressions. 2. Use functions (see below) to encapsulate the procedural description. This has the disadvantage of precluding access to memories. * ORDER OF EVALUATION Suppose input i; wire a; reg b; reg [2:0] c; Compare assign a = b & (c == 4); always @ (posedge clock) begin b = i; c = c + (b & ~a); end to assign a = b & (c == 4); always @ (posedge clock) b = i; always @ (posedge clock) c = c + (b & ~a); In the latter c will not exceed 4 if started from 0. In the former, however, it will. The problem is that a is computed using the old value of b, while c is computed using the new one. * MSB AND LSB Stick to one convention. That is, declare all your vectors as reg [N:0] myreg; or all as reg [0:N] myreg; Avoid mixing the two styles to prevent unreliable translation. * FUNCTIONS AND TASKS It is important to understand how vl2mv handles these constructs to make effective use of them. A function is translated into a .model construct in blif-MV. Even though in general the variables of a module are visible inside a function nested in the model, this is not true of vl2mv. The restriction can be circumvented by passing the relevant information to the function in the form of parameters. However, this does not work for memories, which cannot be passed as parameters. Another restriction of functions is that they cannot return a value from an enumerated type. One practical consequence is that one cannot use a function to encapsulate the next state logic of an FSM in a function if the states are from an enumerated type. A task is flattened into the enclosing module by vl2mv. Hence, one can refer to the variables of the enclosing module---including memories---inside a task. On the other hand, tasks return no values, and can only be invoked from within always blocks. * FOR STATEMENTS Only data-independent loops are allowed by vl2mv, which unrolls all such loops at compilation time. This is not so much a limitation of vl2mv, as a limitation of blif-MV. On the other hand, vl2mv is also unnecessarily restrictive. For instance, assuming that N is constant, for (i = 0; i < N; i = i + 1) if (index == i) a = b[i]; is not allowed, even though, for, say, N=2, this is equivalent to the legal if (index == 0) a = b[0]; if (index == 1) a = b[1]; It is not easy to predict what vl2mv will accept. One can only try and check the result. Another unnecessary restriction is that multiplications and divisions are not allowed on the loop indices. Hence, the following is not allowed. for (i = 0; i < N; i = i + 1) a[i] = i * (i-1) / 2; * BIT SELECTION Vl2mv allows one to address a memory with a variable address, as in reg [N-1:0] memory[0:M-1], data; reg [L-1:0] address; // 2**L = M data = memory[address]; However, vl2mv does not allow one to select individual bits or bits slices with variable indices. This is one of the most serious limitations of vl2mv, because it also affects variable shifts. See also the section on parameterization below. * PARAMETERIZATION The original Verilog language had very limited support for parameterization of descriptions. Vl2mv is based on this original language, and adds some restrictions of its own. It is particularly difficult to parameterize descriptions that select one bit, or one bit slice, from a vector, based on the value of some other variable. One cannot write reg [N:0] myreg; reg [L:0] index; reg bit; bit = myreg[index]; If N is not a parameter, but a constant (say, 4), one can write function select; input [N:0] in; input [L:0] sel; begin: _select if (sel == 0) select = in[0]; else if (sel == 1) select = in[1]; ... else if (sel == 4) select = in[4]; else select = 0; // default end endfunction // select One would like to parameterize this function by replacing the series of "if"'s with a "for" loop, but, as described above, vl2mv does not allow it. One solution is to use a memory instead of a vector, but one has to keep in mind that memories cannot be passed to functions or to other modules. * SHIFTS Vl2mv does not support ">>" and "<<" by default. Shift by a fixed amount can be obtained by concatenation: reg [N:0] myreg; myreg = {1'b0,myreg[N:1]}; Specifying the length of the constant (the "1" before the tick mark) is important to avoid unreliable translation. Parameterized shifts are also possible: reg [N:0] myreg; myreg = {{P{1'b0}},myreg[N:P]}; // P < N Variable shifts pose similar problems to indexing into a vector. A function can be used for the non-parameterized cases. * PADDING OF VALUES Suppose you have declared: reg [4:0] a, b; reg [2:0] c; Then a = b + c; produces a different result from a = b + {2'b0,c}; You probably want the latter. * NEGATIVE NUMBERS Always specify the number of bits when negative numbers are involved. With a three-bit register like this: reg [2:0] r; writing initial r = -1; produces incorrect blif-MV. Use initial r = -3'b1; instead. * THE $ND SYSTEM TASK VERSUS PRIMARY INPUTS There are two way to get nondeterministic behavior. 1. To use the $ND system task. 2. To use a primary input. The $ND is useful when the nondeterministic choice is made deep in the hierarchy of modules. Bringing in an input from the top level, especially when it's just one bit, is usually much more cumbersome than using an $ND. Besides, the use of $ND declares unambiguously the intention to model nondeterministic behavior. On the other hand, using $ND prevents you from simulating your description with standard Verilog simulators. Unless you have already given up that possibility, this should give you reason to ponder. With primary inputs it's also easier to model multi-way choices when there are many choices. * INITIALIZATION Initialize every register, even those whose initial value is immaterial, to avoid unreliable translation. If you want multiple initial states, use $ND assignments in the "initial" block or make the initial state depend on primary inputs. (See previous section on $ND versus primary inputs.) If the initial states are described by an arbitrary predicate over the state variables, one can use the approach demonstrated in the following example. // This module illustrates a coding style that can be used to specify an // arbitrary set of initial states. // // This particular model has two state variables, a and b, and two valid // initial states, 00 and 11. The model itself simply swaps the values of // a and b. Hence, the initial states are also the only reachable states. module relinit(clock); input clock; reg a,b; // This function returns 1 if the inputs correspond to a valid initial // state. function valid; input a; input b; begin: _valid valid = a == b; end endfunction // valid initial begin // Start by assuming all states initial. a = $ND(0, 1); b = $ND(0, 1); // Then remap invalid initial states to valid one. if (!valid(a,b)) begin a = 0; b = 0; end end // initial begin always @ (posedge clock) begin a = b; end always @ (posedge clock) begin b = a; end endmodule // relinit * LATCHING VARIABLES FOR THE MODEL CHECKER VIS requires that all variables that appear in CTL formulae or fairness constraints (which are also CTL formulae) be ultimately expressible in terms of state variables only. It is therefore often necessary to "latch" some primary inputs so that properties can refer to their values. If the input value is required in a fairness constraint, it is convenient to use the input rather than the latched version in the rest of the Verilog description. (Assuming that this is what one would do if it were not for VIS's requirement.) Indeed, when checking invariants that do not require fairness constraints, VIS will automatically eliminate the extra variables from the model. A similar observation applies to "regs" that store intermediate results in an "always" block. Consider the following piece of code. always @ (posedge clock) begin found = 0; for (i = 0; i < N; i = i + 1) begin if (data[i] == 0) found = 1; end if (found) flag = ~flag; end Variable "found" must be declared as a "reg." However, if it is not used elsewhere in the module, the value stored in the register is never used. Such a register will be in the model used by compute_reach, but will be dropped in model checking unless the property refers to "found" explicitly. If the property refers to "flag," but not "found," the latch for the latter is not included in the reduced FSM used by VIS. This is in spite of the apparent dependence of "flag" on "found." The reason is that "flag" depends on the next value of "found," which is in turn a combinational function of "data" only. * ARGUMENTS TO MODULE INSTANCES AND PATHNAMES Vl2mv does not allow to use the "." operator of Verilog to refer to signals in other modules. The former limitation (hierarchical names) is a logical consequence of the way Verilog modules are translated into blif-MV .model's. * PASSING PARAMETER VALUES TO MODULE INSTANCES Consider the following piece of code. module a(...); parameter P = 4; ... b #(P) my_b(...); ... endmodule // a module b(...); parameter P = 8; ... endmodule // b This description will cause vl2mv to generate a larger .mv file than if P had been given the same value in both a and b. If the same module is instantiated with different parameter values, one has no choice. Otherwise, it is advisable to use the same value for P in both a and b. * SINGLE BIT ADDRESSES If a memory has only two locations, one bit suffices for the addresses. To avoid incorrect translation, however, one-bit variables used to address memories should be declared as "addr" in the following code fragment: reg mem[0:1]; reg [0:0] addr; ... mem[addr] = ...