The state justification problem is the decision problem of finding a
sequence of states and input values that satisfy an output condition
for a given state machine or RTL description. In such problems, there
always exist optimal state sequences that require a minimum number of
clock cycles to reach the desired state.
As Boolean decision problems, state justification problems can be
expressed as satisfiability problems (SAT) by using the time-frame
expansion algorithm. Boolean SAT or BDD-based techniques are bit-level
decision procedures commonly used by industrial hardware verification
tools. Unfortunately, these approaches are not efficient enough,
because they do not inherit the word-level information from the RTL
design. Recent approaches to the SAT problem are addressed to RTL
designs containing instances of both, word-level arithmetic blocks for
data flow, and bit-level Boolean logic for control flow. These
approaches transform the whole SAT problem for an RTL description into
a mixed integer linear program (MILP).
This paper presents a new approach that finds in a single step, the
optimum input sequence for a given RTL description to reach a desired
state. This is accomplished by applying a novel time-frame expansion
method that guarantees an optimal solution and avoids performing
time-frame expansions iteratively.
Experimental results will demonstrate that the proposed methodology
can solve any state justification problem in one step for complex
FSMs. The main application of this procedure is the test pattern
generation, where the main problem is to reduce the length of test
sequences that verifies a microcircuit.
Real time image processing is a key issue in nowadays multimedia applications. Image filtering and video coding are two basic applications in image processing. Their algorithms are computationally expensive due to both, the number of points of each frame to be processed, and the calculation complexity per point. The VLSI implementation of these algorithms leads to special architectures that are based on systolic arrays, and whose implementation is greedy in silicon area. In this paper, we propose a configurable and bidimensional pipelined VLSI architecture that supports mathematical morphology operations and the block matching algorithm. Remarkable advantages include low power consumption, and a regular and compact design (in terms of core active area) versus the traditional systolic architecture. The architecture is adequate for both morphological image filtering and video compression, depending on the hardware resources of the processing elements. The main advantage of this bidimensional pipeline architecture is the area saving compared with the systolic array implementation. Total area saving was presented in terms of the number of bits of the FIFO memories that can be eliminated. The proposed architecture was verified at high level in C++, at RTL level using Verilog and at C++/RTL level using DEMETER. Required cycle times was measured for a real time morphological filter per dilation/erosion operation, as a function of the incoming resolution. Physical layouts were obtained for the basic slice of the processing element and for the systolic array using the technology of 0,35 microns CMOS from AMS.
System verification is an important issue to do at every design step to ensure the complete system correctness. The verification effort is becoming more time-consuming due to the increase in design complexity. New environments are necessary to reduce the complexity of this task and, most importantly, reduce the time to develop it. Among the languages used in verification, C++ is powerful enough for encapsulating the necessary concepts in a set of classes and templates. This work introduces a framework that allows describing and verifying highly complex systems in a user-friendly and speedy way with C++ classes. These encapsulate hardware description and verification concepts and can be reused throughout a project and also in various development projects. Furthermore, the resulting libraries provide an easy-to-use interface for describing systems and writing test benches in C++, with a transparent connection to an HDL
simulator. VESTA includes an advanced memory management with an extremely versatile linked list. The linked list access mode can change on-fly to a FIFO, a LIFO or a memory array access mode, among others. Experimental results demonstrate that the basic types
provided by our verification environment excel the features of
non-commercial solutions as Openvera or TestBuilder and commercial solutions such as 'e' language. Besides, the results achieved have shown significant productivity gain in creating reusable testbenches and in debugging simulation runs.
A new transient macromodel for the cells used in DCFL GaAs and CMOS digital design is introduced in this paper. The numerical solution determines accurate propagation delay times. The macromodel is based on the differential equation for the output voltage in terms of currents and capacitances. An straightforward treatment of the differential equation for an inverter in DCFL GaAs and CMOS has been obtained. It could be resolved numerically by a 4th order Runge Kutta method. Good agreement is obtained between the HSPICE simulation and the computation of the propagation delays for DCFL GaAs and CMOS basic gates: INV, NOR, OR and NAND. There is no error between HSPICE and our computation of propagation delay time for the high to low (tphl) and low to high (tplh) transitions. The propagation delay times for two types of transition were measured and compared with HSPICE. The results demonstrate that our approach matches with HSPICE with no error. The numerical method was programmed in C language. In addition, computation time analysis is provided and numerical solution is several orders of magnitude faster than HSPICE. Work is in progress to obtain the macromodel of a standard cell library for digital application both for a 0.6 microns E/D GaAs process (H-GaAsIV) from Vitesse Semiconductor and for a 0.18 microns logic/mixed-signal CMOS process (1P6M) from TSMC Corp.
A system-level verification methodology for advanced switch fabrics is introduced in this paper. Verification is getting more time-consuming as design complexity increases and typically consumes over half of the design effort. Writing testbenches in an ad-hoc verification environment, such as Verilog, VHDL or in C/C++ using PLI directly, is tedious, unproductive and the reusability is low. Time-to-market is critical at chip-level verification, if we add the short life cycles and the changing standards, the design and verification of new products require new design and verification tools. As result of our methodology a verification framework is also presented. The decomposition of each interface of the switch fabric allows the reconfiguration of the framework, when there is a new revision of one design. This idea promotes the reuse of the main interface code and verification statements. The development of the verification framework in C++, 'e' and Verilog demonstrates that our methodology can be applied independently of the programming language. New features, added to the framework such as error insertion, give a highest control over the verification and they enhance the verification coverage in corner case mode. On the other hand, the golden reference layer is the key of the automatic mode, because a high level model can be used as reference to check the correctness of the DUV automatically and the synchronization issues are resolved between the different simulator natures. Several commercial and non-commercial advanced switch fabrics have been verified using this method. The highest complexity verified circuits were VSC882/VSC872 (GigaStream Chip Set). The usefulness of the proposed methodology is demonstrated by GigaStream Chip Set functional success and the saving of a 60% in the verification time per effort unit. In general, given a programming language, the improvement of using our methodology is around a 40% in verification time per effort unit.