This paper presents experimental and computational results of oxy-fuel burner operating on classical flame and flameless mode for heat release rate of 26kW/m3. The uniqueness of the burner arises from a slight asymmetric injection of oxygen at near sonic velocities. Measurements of temperature, species, total heat flux, radiative heat flux and NOx emission were carried out inside the furnace and the flow field was computationally analyzed. The flame studies were carried out for coaxial flow of oxygen and fuel jets with similar inlet velocities. This configuration results in slow mixing between fuel and oxygen and the flame is developed at distance away from the burner and the flame is bright/white in colour. In the flameless mode a slight asymmetric injection of the high velocity oxygen jet leads to a large asymmetric recirculation pattern with the recirculation ratio of 25 and the resulting flame is weak bluish in colour with little soot and acetylene formation. The classical flame in comparison is characterised by soot and acetylene formation, higher NOx and noise generation. The distribution of temperature and heat flux in the furnace is more uniform with flameless mode than with flame mode.

Functional validation is one of the most complex and expensive tasks in the current processor design methodology. A significant bottleneck in the validation of processors is the lack of a golden reference model. Thus, many existing approaches employ a bottom-up methodology by using a combination of simulation techniques and formal methods. We present a top-down validation approach using a language-based specification. The specification is used to generate the necessary reference models for processor validation using symbolic simulation. We applied our methodology for property checking as well as equivalence checking of microprocessors.

This article, from the Motorola (now Freescale) PowerPC design group, presents an interesting synergy among test, equivalence verification, and constraints. The authors use RTL, gate, and switch models of a design in two different flows one for test and one for functional verification to show that rectifying constraints and merging tests between the-two flows saves significant presilicon debug effort.

A major challenge in today's functional verification is the lack of a formal specification with which to compare the RTL model. We propose a novel top-down verification approach that allows specification of a design above the RTL. From this specification, it is possible to automatically generate assertion models and RTL reference models. We also demonstrate that symbolic simulation and equivalence checking can be applied to verify an RTL design against its specification.

This paper presents the reasoning behind eliminating full-chip gate/switch-level simulations for microprocessors/digital system designs and utilizing RTL models for the purpose, provided formal boolean equivalence between RTL and gate/switch-level models have been established using symbolic simulation for all blocks that comprise the chip. No logic bug should go undetected if only RTL models are used for full chip simulations provided existing design methodologies are enhanced to incorporate a constraints checking flow coupled with a rigorous circuit metastability/contention prevention flow.

Formal tools are either too labor intensive or are completely impractical for industrial-size problems. This paper describes two formal verification tools used within Motorola, Versys2 and CBV, that challenge this assertion. The two tools are being used in current design verification flows and have shown that it is possible to seamlessly integrate formal tools into existing design flows.

In Motorola's High Performance Design Center, two verification flows are often used to verify correctness of custom designed blocks. The first is an equivalence checking flow, and the second is a manufacturing test pattern generation/simulation flow. The two flows are often disconnected resulting into silicon failures on manufacturing test vector suites. Our aim is to analyze the disconnect and to arrive at a technique that bridges the gap between the two verification flows by validating the correctness of manufacturing test patterns. This reduces time to market by cutting down on precious silicon debug time by eliminating redundant defect fixes. Our experimental results were obtained from a set of custom designed circuits of a Motorola MPC74XX microprocessor.

Several bottom-up validation techniques have been proposed to formally verify the implementation of a microprocessor by comparing the pipelined implementation with its Instruction-Set Architecture (ISA) specification model, or by deriving the ISA model from the implementation. We present a top-down validation approach using symbolic simulation. We define a set of properties and verify the correctness of the processor by verifying if the properties are met. We applied our methodology to verify several properties on a Memory Management Unit (MMU) of a microprocessor that is compliant with the PowerPC instruction-set architecture to demonstrate the usefulness of our approach.

Equivalence checking between Register Transfer Level (RTL) descriptions and transistor level descriptions of custom memories is an important step in the design flow of high performance microprocessors. Equivalence checking can be done with or without the knowledge of state mapping between the two descriptions. We present evidence that because of state mapping, our verification technique exercises system behavior that exposes hard-to-detect bugs that might otherwise go undetected.This paper defines Crossover Bugs (CB's) that can be present in scan-based custom designs and that are inherently hard-to-detect without state mapping. We demonstrate that such bugs can be missed by equivalence checking techniques that do not have state mappings between the two descriptions. By identifying the state correspondences between the RTL and the transistor implementation of custom memories, a more rigorous equivalence check can be performed compared to traditional equivalence checking methods such as product machine constructions. We also compare the time and memory complexities of crossover bug detection capability of the two equivalence checking approaches.We conclude with experimental results of CB detection on some of the custom designed embedded memories of Motorola's MPC 7455 microprocessor (compliant with IBM's PowerPC instruction set architecture).

CAD tool designers have given priority to providing features that will let circuit and logic designers use this custom-memory formal verification and analysis tool without a steep learning curve. This article discusses a few fundamental design decisions behind the successful deployment of a second-generation formal custom-memory equivalence-checking tool, Versys2, in the PowerPC design flows. The Versys2 symbolic simulator was developed at Motorola for verifying equivalence between register-transfer-level (RTL) designs and custom transistor circuit schematics.

This paper describes the use of Symbolic Trajectory Evaluation (STE), a modified form of symbolic simulation, to verify the equivalence between RTL and transistor-level representations of on-chip custom memories for the latest PowerPC microprocessor. The validation of embedded memories and their associated control logic poses a special problem for traditional formal equivalence checking tools due to the inherently sequential and self-timed nature of the internal control logic and the large number of state-holding elements.The use of the VERSYS STE engine to validate these custom memories is illustrated. We present our array verification methodology, discuss some of the results of our approach, and outline plans for future development.

Due to the high cost of correcting errors in a final product, there is a growing impetus in industry towards methodologies that can yield correct designs in the first manufacturing run. Design validation methodologies that combine simulation techniques with formal reasoning can be effective in ensuring correct operation of software and hardware systems. We show why simulation is necessary to complement formal mathematical reasoning in verifying certain classes of custom designed circuits. We present a validation methodology for PowerPC custom memories based on symbolic simulation.

For verifying complex sequential blocks such as microprocessor embedded arrays, the formal method of symbolic trajectory evaluation (STE) has achieved great success in the past. Past STE methodology for arrays requires manual creation of "assertions" to which both RTL view and the actual design should be equivalent. In this paper, we describe a novel method to automate the assertion creation process which improves the efficiency and the quality of array verification. Encouraging results on recent PowerPC arrays will be presented.

Design constraints are artifacts that model an environment of a design under verification by restricting input stimuli to plausible valuations. Judicious usage of design constraints can be effective in eliminating false verification results. Given a particular verification problem, however, it is a difficult proposition to write down all the necessary constraints. We present a technique for automatic generation of design constraints from simple user-provided information about potential design environments. Our method generates a set of design constraints representing varying degrees of assumptions about potential environments of a dynamic circuit. We also present experimental results on verification of custom designed embedded dynamic circuits taken from the Motorola MPC7455(1) microprocessor.