62 resultados para formal verification


Relevância:

20.00% 20.00%

Publicador:

Resumo:

The preparation of 6-endo-formyl-1,3,3-trimethylbicyclo[2.2.2]octan-2-one 7 and 6-endo-acetyl-1,3,3-trimethylbicyclo[2.2.2]octan-2-one 8, the two key intermediates for the synthesis of patchouli alcohol 1 and norpatchoulenol 2, is reported by a simple and short method from 2-methylbenzoic acid.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

This paper is concerned with off-line signature verification. Four different types of pattern representation schemes have been implemented, viz., geometric features, moment-based representations, envelope characteristics and tree-structured Wavelet features. The individual feature components in a representation are weighed by their pattern characterization capability using Genetic Algorithms. The conclusions of the four subsystems teach depending on a representation scheme) are combined to form a final decision on the validity of signature. Threshold-based classifiers (including the traditional confidence-interval classifier), neighbourhood classifiers and their combinations were studied. Benefits of using forged signatures for training purposes have been assessed. Experimental results show that combination of the Feature-based classifiers increases verification accuracy. (C) 1999 Pattern Recognition Society. Published by Elsevier Science Ltd. All rights reserved.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

A short approach to (+/-)-2-pupukeanone, starting from 2,6-dimethylcyclohexenone employing a combination of Michael-Michael reaction and an intramolecular rhodium carbenoid C-H insertion as key reactions, is described.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

We give a detailed construction of a finite-state transition system for a com-connected Message Sequence Graph. Though this result is well-known in the literature and forms the basis for the solution to several analysis and verification problems concerning MSG specifications, the constructions given in the literature are either not amenable to implementation, or imprecise, or simply incorrect. In contrast we give a detailed construction along with a proof of its correctness. Our transition system is amenable to implementation, and can also be used for a bounded analysis of general (not necessarily com-connected) MSG specifications.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

An efficient ring closing metathesis (RCM.) reaction based approach was developed for the spiroannulation of cyclopentanes and cyclohexanes and its utility demonstrated in the formal synthesis of the spirosesquiterpenes acorones.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

An enantiospecific formal total synthesis of (-)-ceratopicanol starting from the readily and abundantly available monoterpene (R)-limonene is described. A combination of Claisen rearrangement-intramolecular diazo-ketone cyclopropanation-regiospecific reductive cyclopropane cleavage reactions are employed for the stereo- and regiospecific generation of the two vicinal ring junction quaternary carbon atoms.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

An efficient strategy for the contruction of spiro[4.5] decanes is described and involves a bridgehead substitution of a methoxyl group by a methyl group followed by an oxidative cleavage of the tricyclo[5.2.2.0(1,5)] undecane 25 to produce the spiro[4.5] decanes 31 & 32 which are intermediates in the synthesis of acorone. A novel one-pot conversion of alpha-methoxy carboxylic acid to alpha-methyl carboxylic acid is described.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

Enantioselective formal synthesis of macrolactone palmerolide A, a polyketide marine natural product, is described. Key strategies in the synthesis include the oxidative furan ring-opening of a chiral furyl carbinol for the installation of the 1,4-dienol core and a Jung nonaldol-aldol reaction for the dienamide core.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

Verification is one of the important stages in designing an SoC (system on chips) that consumes upto 70% of the design time. In this work, we present a methodology to automatically generate verification test-cases to verify a class of SoCs and also enable re-use of verification resources created from one SoC to another. A prototype implementation for generating the test-cases is also presented.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

The success of an ABV IP depends highly on the associated debugging environment. An efficient debugging environment helps the user to find out the exact location of the failure. Moreover, it provides information to the user in a refined detail of abstraction and permit adequate interaction. It has also been realized that adequate visualization support helps in tracking the behavioral aspects of the Design Under Test (DUT). Currently, the debugging tools provide information in the signal level and do not provide any information about the high-level behavior of the DUT. We present a debugging framework that takes the design specification, assertions and the user intent in a simple format and provides detailed information by processing the design trace on-line, or off-line. We also present a visualization framework to ease the debugging procedure. We have experimented with industrial standard on-chip bus protocols that ensure that this utility can be incorporated successfully in the present functional verification flow.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

We analyze the AlApana of a Carnatic music piece without the prior knowledge of the singer or the rAga. AlApana is ameans to communicate to the audience, the flavor or the bhAva of the rAga through the permitted notes and its phrases. The input to our analysis is a recording of the vocal AlApana along with the accompanying instrument. The AdhAra shadja(base note) of the singer for that AlApana is estimated through a stochastic model of note frequencies. Based on the shadja, we identify the notes (swaras) used in the AlApana using a semi-continuous GMM. Using the probabilities of each note interval, we recognize swaras of the AlApana. For sampurNa rAgas, we can identify the possible rAga, based on the swaras. We have been able to achieve correct shadja identification, which is crucial to all further steps, in 88.8% of 55 AlApanas. Among them (48 AlApanas of 7 rAgas), we get 91.5% correct swara identification and 62.13% correct R (rAga) accuracy.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

Continuous advances in VLSI technology have made implementation of very complicated systems possible. Modern System-on -Chips (SoCs) have many processors, IP cores and other functional units. As a result, complete verification of whole systems before implementation is becoming infeasible; hence it is likely that these systems may have some errors after manufacturing. This increases the need to find design errors in chips after fabrication. The main challenge for post-silicon debug is the observability of the internal signals. Post-silicon debug is the problem of determining what's wrong when the fabricated chip of a new design behaves incorrectly. This problem now consumes over half of the overall verification effort on large designs, and the problem is growing worse.Traditional post-silicon debug methods concentrate on functional parts of systems and provide mechanisms to increase the observability of internal state of systems. Those methods may not be sufficient as modern SoCs have lots of blocks (processors, IP cores, etc.) which are communicating with one another and communication is another source of design errors. This tutorial will be provide an insight into various observability enhancement techniques, on chip instrumentation techniques and use of high level models to support the debug process targeting both inside blocks and communication among them. It will also cover the use of formal methods to help debug process.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

An enantiospecific formal total synthesis of the 5-8-5 tricyclic diterpene fusicoauritone has been accomplished, starting from 5-isopropyl-2-methylcyclopent-1-enemethanol [available in three steps from (R)-dihydrolimonene] employing two ring-closing-metathesis reactions for the construction of the eight- and five-membered rings.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

Null dereferences are a bane of programming in languages such as Java. In this paper we propose a sound, demand-driven, inter-procedurally context-sensitive dataflow analysis technique to verify a given dereference as safe or potentially unsafe. Our analysis uses an abstract lattice of formulas to find a pre-condition at the entry of the program such that a null-dereference can occur only if the initial state of the program satisfies this pre-condition. We use a simplified domain of formulas, abstracting out integer arithmetic, as well as unbounded access paths due to recursive data structures. For the sake of precision we model aliasing relationships explicitly in our abstract lattice, enable strong updates, and use a limited notion of path sensitivity. For the sake of scalability we prune formulas continually as they get propagated, reducing to true conjuncts that are less likely to be useful in validating or invalidating the formula. We have implemented our approach, and present an evaluation of it on a set of ten real Java programs. Our results show that the set of design features we have incorporated enable the analysis to (a) explore long, inter-procedural paths to verify each dereference, with (b) reasonable accuracy, and (c) very quick response time per dereference, making it suitable for use in desktop development environments.