HDL-Based Tools and Environments:Verification Tools

By -
Verification Tools

As mentioned before, there are two ways to inspect the correctness of the design steps: simulation and verification. Simulation methods were described in Section 96.1 and this section is dedicated to the verification methods. Verification methods are classified into two categories:

• Assertion-based verification: In design validation using simulation, the simulation results should be inspected manually. In an assertion-based verification, assertion monitors are used to check the simulation results continuously. The designer provides several properties to show the correct behavior of a circuit and develops the assertion monitors to check that these properties are not violated. When a design property is violated, the assertion triggers and alerts the designer. A set of common assertion monitors are provided in the open verification library (OVL).

• Formal verification: After completing a design, the designer provides a set of properties to show the correct behavior of the design. The process of property checking is called formal verification. A formal verification tool tries to match a property with the specification of a design and if it is unsuccessful, it finds the input conditions that make the property fail.

Comments

Post a Comment

Popular posts from this blog

Square wave oscillators and Op-amp square wave oscillator.

By -
Image
Square wave oscillators If Fourier analysis is performed on a square wave it is found that the waveform is composed of many harmonics of the fundamental frequency. This rich harmonic content makes the square wave particularly useful as a quick test of amplifier performance. Examples of possible results are shown. The simplest way to produce a square wave is to make a sine wave oscillator in one of the ways described earlier, then feed the output to some form of squaring circuit such as a Schmitt trigger. This is the method adopted in most commercial sine/square wave generators. There are, however, several circuits for square wave oscillators and a description of the most common follows. Multivibrator Technically the multivibrator is a relaxation oscillator, working on the charging of a capacitor through a resistor. If a negative edge is applied to the circuit in (a), transistor TR 1 turns off the for time taken for the base voltage to return to 0 V. If the voltage step is
Read more

Adders:Carry Look-Ahead Adder.

By -
Image
Carry Look-Ahead Adder As previously stated, the carry, c i +1, produced at the i -th position is calculated as c i +1 = x i · y i ∨ c i ·( x i ⊕ y i ). This means that a carry is generated if both x i and y i are 1, or an incoming carry is propagated if one of x i and y i is 1 and the other is 0. Therefore, letting g i denote x i y i , we have c i +1 = g i ∨ c i p i , where p i = x i ⊕ y i . Here, g i is the formula for the carry generation condition at the i -th position, i.e., when g i is 1, a carry is generated at this position. Substituting g i –1 ∨ p i –1 c i –1 for c i , we get A carry look-ahead adder can be realized according to this expression, as illustrated in Figure 41.10 for the case of four bits [21]. According to this expression, c i +1’s are calculated at all positions in parallel. It is hard to realize an n -bit carry look-ahead adder precisely according to this expression, unless n is small, because maximum fan-in and fan-out restriction is violated at higher
Read more