Considering Static Functional Verification Of Digital Systems For Hdl Based Courses

Functional verification of VLSI designs is known to be a highly time-consuming phase of the design cycle. Furthermore, with increasing complexity of ASICs and programmable ICs, this problem is becoming even more challenging. An emerging approach, which helps shorten the verification cycle, is the formal approach in which mathematical techniques are used to prove properties about a design. Due to the fact that formal checks are exhaustive and no test-vectors are needed, supporting tools have gained significant momentum as an add-on solution to simulation. It is the focus of this paper to present the formal or static approach and encourage use of the available tools in design projects for Senior/Graduate-level HDL-based courses. Advantages of the static approach will be discussed by presenting property formulation for a few RTL designs. Moreover, the property language PSL (Property Specification Language), which has the promise of becoming an IEEE standard, will be used in presenting property formulations. Introduction: A widely practiced approach for functional verification of digital designs is the use of simulation tools and test-bench models. Although simulation is a very effective solution, designers today are continuously faced with the challenge of exhaustive and timely verification of large systems. Many designs are taped-out with corner bugs, which is the result of non-exhaustive simulation coverage. Furthermore, with the growing complexity of IC designs and programmable parts, simulation runs are becoming prohibitively long and non-convergent. One solution, which was first commercially introduced in the mid 1990s, is the use of static tools [1] in addition to simulation. The Static approach consists of formulating properties about a design (instead of using test-benches) and proving those properties or assertions using mathematical proof techniques. A proven property is exhaustive in that it holds for all possible states, and sequences of inputs of the design. In today’s design community, static functional verification is gaining momentum as a solution for block-level verification of IC designs. The premise is that if individual blocks in a design are proven correct, then system-level verification will be a more manageable task. However, due to the capacity limitations of formal techniques, simulation is still needed for the system-level verification, where the size of designs can be prohibitively large for any formal tool to be useful. Considering the significance of the verification problem and the emergence of static tools as an add-on solution to simulation, it is the focus of this paper to present the static approach and P ge 10344.1 “Proceedings of the 2005 American Society for Engineering Education Annual Conference & Exposition Copyright2005, American Society for Engineering Education” encourage the use of available tools in the design projects for Senior/Graduate-level HDL-based courses. All commercial static tools today support Verilog [3] or VHDL [4] , both IEEE standards, as the language to describe designs. Moreover, efforts are underway to formulate and standardize the property language PSL (Property Specification Language) [2] , which will support both the Verilogand VHDL-flavor. Most verification tools today support the existing definition of PSL. Advantages of the static approach will be discussed in this paper by presenting property formulation for a few RTL designs. These advantages are key in finding costly functional problems before proceeding to the system-level verification. Typical design scenarios are presented and properties are developed in order to do an exhaustive functional verification statically. With PSL gaining momentum as a property specification language of choice, properties in this paper will be developed using PSL constructs, including temporal expressions and sequences. Furthermore, the results of verifying a set of properties and uncovering functional bugs will be presented. It will be evident from the contents of this paper that static tools can be readily integrated into HDL-based courses to complement simulation. Learning PSL and property formulation will structure the verification efforts in that it will promote a discipline for exhaustive functional coverage. This discipline is equally applicable to formulating simulation test bench models. Property Formulation: The most fundamental difference between the static and dynamic approaches is that the latter uses a set of stimulus input vectors to drive a design and produces a set of corresponding output values. Subsequently, these output values would have to be inspected for expected behavior. Clearly, the completeness of functional coverage is dependent upon the quality and completeness of the input stimuli. In the static approach, however, the verification is accomplished by first formulating what is referred to as properties, which capture what the design should always do and what it should never do. Subsequently, the tool will prove whether a given property will hold under all input and state conditions. If not, a trace or a set of input and state conditions will be produced illustrating why the property failed. No test bench or inspection of any simulation output is required. A property is a logical expression similar to those in Verilog or VHDL. Additionally, a property must capture temporal relationships among expressions. A commonly used operator in property formulation is the logical implication, which can be defined to include a number of temporal characteristics. The following table illustrates the implication operators supported by PSL. In this table, both A and B represent expressions that may take several cycles before their truthvalue is established. Operation Function A -> B If A is true then B must hold. Both A and B are evaluated concurrently A <-> B If A is true then B must hold and if B is true then A must hold. Both A and B are evaluated concurrently A |-> B If A is true then B must hold. B is evaluated in the last cycle of A A |=> B If A is true then B must hold. B is evaluated after the last cycle of A P ge 10344.2 “Proceedings of the 2005 American Society for Engineering Education Annual Conference & Exposition Copyright2005, American Society for Engineering Education” Consider a Moore state machine, which detects “110” on input din and asserts its output match if a match is found. Verilog statements for this state machine are listed below. always @(posedge clk) shift_reg <= {shift_reg[1:0], din}; assign match = shift_reg[2] && shift_reg[1] && !shift_reg[0]; In general, the best approach is to start from the specification and formulate PSL assertions that capture the expected functionality. Moreover, in large designs, knowledge of the design architecture is helpful in achieving full coverage efficiently. The following property reflects the expected behavior. assert always (din && (next din) && (next[2] !din)) -> (next[3] match); Furthermore, it should be proved that there exists no other condition under which a match is detected. This is accomplished by reversing the original property, as shown below. assert always (next[3] match) -> (din && (next din) && (next[2] !din)); Uses of the PSL “next” operator, in the above assertions, capture the temporal relationships on both sides of the implication operator. The entire property spans four clock cycles, which includes the present cycle and three cycles into the future. The truth-value of the left-hand-side in the first property is established in three cycles and that of the right-hand side in four cycles. The following two assertions make use of the other PSL implication operators but capture the same identical behavior as the above assertion. assert always {din; din; !din} |-> {true; match}; assert always {din; din; !din} |=> {match}; Both sides of the implication consist of a sequence, enclosed in {...}. A sequence specifies any number of events, which are to take place in multiple clock cycles. As shown, a semi colon separates each event. For example, the sequence “{din; din; !din}” specifies the expected input pattern and in case of “|=>”, the right-hand-side expression is evaluated after the input pattern is detected. However, in case of “|->”, the right hand side is evaluated concurrent with the cycle in which “!din” is detected, hence the use of the keyword “true”. All of the above properties pass verification. In addition to considering design specification when formulating properties, one can prove useful design characteristics that may result in updating the specification and/or finding a functional error. A useful assertion for this design is to prove that once a match is found, there shall be no more match for at least the pursuing two clock periods. assert always match -> (next_a[1:2] !match); Page 10344.3 “Proceedings of the 2005 American Society for Engineering Education Annual Conference & Exposition Copyright2005, American Society for Engineering Education” However, an assertion, which checks for at least three cycles between consecutive matches, fails as expected and a signal trace showing wire and state values for four clock cycles is generated. assert always match -> (next_a[1:3] !match); t0 t1 t2 t3 din 1 1 0 0 match 1 0 0 1 shift_reg[2:0] 110 101 011 110 The shift register points out that a pattern of “110” has already been received and as a result match is asserted at time t0. Moreover, starting at time t0 another pattern of “110” is initiated resulting in a match at time t3, thus violating the property. Formal Verification vs. Simulation: Formal or static tools provide certain functional coverage, which is not readily achievable by simulation, if at all possible. This is illustrated in the verification of the following Verilog description, which is a 4-bit BCD counter with load and enable inputs. module cnt(clk, rst, load, enable, cout, data); input clk, rst, load, enable; input [3:0] data; output reg [3:0] cout; alw