Formal Verification of Full-Wave Rectifier: A Case Study

We present a case study of formal verification of full-wave rectifier for analog and mixed signal designs. We have used the Checkmate tool from CMU [1], which is a public domain formal verification tool for hybrid systems. Due to the restriction imposed by Checkmate it necessitates to make the changes in the Checkmate implementation to implement the complex and non-linear system. Full-wave rectifier has been implemented by using the Checkmate custom blocks and the Simulink blocks from MATLAB from Math works. After establishing the required changes in the Checkmate implementation we are able to efficiently verify, the safety properties of the full-wave rectifier.

Potassamide induced in situ alkylation of 5,6-dihydroisoquinolines: Structure of products

Potassamide induced in situ alkylation of 1-alkyl- 4-cyano-3-methoxy-5,6-dihydroisoquinolines (2a & 2b) with alkyl iodides (CH3I, CH3CH2I & cyclohexyl iodide) gave the 5-alkyl- and 5,9-dialkyl-5,6-dihydroisoquinolines (4–ad & 3a–e), isoquinoline derivatives, (5a–b) and diastereomeric mixture of 4- alkyl-1,2,3,4-tetrahydroisoquinolin-3(2H)-ones (6a–e & 6′a–e). Structures were assigned on the basis of spectral data [Mass, 1H & 13C NMR, 2D NOESY & HC-COLOC]. Amide induced in situ alkylation of compounds 3a and 4a with CH3I gave in almost quantitative yield the dimethylated compounds 3d and 3a respectively. While KNH2/liq.NH3 methylation of 1,2- dihydroisoquinoline, 1 with CH3I gave the mixture of compounds, 6a & 6′a and the isoquinoline derivative 5a, NaH/benzene reaction of 1 with CH3I gave exclusively 5a. N-methylation of the mixture of compounds 6a & 6′a with NaH/CH3I gave the methylated derivatives, 7 & 8. A suitable mechanism has been proposed for the formation of products.

Towards formal verification of analog mixed signal designs using SPICE circuit simulation traces

An extension to a formal verification approach of hybrid systems is proposed to verify analog and mixed signal (AMS) designs. AMS designs can be formally modeled as hybrid systems and therefore lend themselves to the formal analysis and verification techniques applied to hybrid systems. The proposed approach employs simulation traces obtained from an actual design implementation of AMS circuit blocks (for example, in the form of SPICE netlists) to carry out formal analysis and verification. This enables the same platform used for formally validating an abstract model of an AMS design, to be also used for validating its different refinements and design implementation; thereby, providing a simple route to formal verification at different levels of implementation. The feasibility of the proposed approach is demonstrated with a case study based on a tunnel diode oscillator. Since the device characteristic of a tunnel diode is highly non-linear with a negative resistance region, dynamic behavior of circuits in which it is employed as an element is difficult to model, analyze and verify within a general hybrid system formal verification tool. In the case study presented the formal model and the proposed computational techniques have been incorporated into CheckMate, a formal verification tool based on MATLAB and Simulink-Stateflow Framework from MathWorks.

Admissible fundamental operators(star)

Let F and G be two bounded operators on two Hilbert spaces. Let their numerical radii be no greater than one. This note investigates when there is a Gamma-contraction (S, P) such that F is the fundamental operator of (S, P) and G is the fundamental operator of (S*, P*). Theorem 1 puts a necessary condition on F and G for them to be the fundamental operators of (S, P) and (S*, P*) respectively. Theorem 2 shows that this necessary condition is also sufficient provided we restrict our attention to a certain special case. The general case is investigated in Theorem 3. Some of the results obtained for Gamma-contractions are then applied to tetrablock contractions to figure out when two pairs (F1, F2) and (G(1), G(2)) acting on two Hilbert spaces can be fundamental operators of a tetrablock contraction (A, B, P) and its adjoint (A*, B*, P*) respectively. This is the content of Theorem 3. (C) 2015 Elsevier Inc. All rights reserved.