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.

Bond graph toolbox for handling complex variable

Bond graph is an apt modelling tool for any system working across multiple energy domains. Power electronics system modelling is usually the study of the interplay of energy in the domains of electrical, mechanical, magnetic and thermal. The usefulness of bond graph modelling in power electronic field has been realised by researchers. Consequently in the last couple of decades, there has been a steadily increasing effort in developing simulation tools for bond graph modelling that are specially suited for power electronic study. For modelling rotating magnetic fields in electromagnetic machine models, a support for vector variables is essential. Unfortunately, all bond graph simulation tools presently provide support only for scalar variables. We propose an approach to provide complex variable and vector support to bond graph such that it will enable modelling of polyphase electromagnetic and spatial vector systems. We also introduced a rotary gyrator element and use it along with the switched junction for developing the complex/vector variable's toolbox. This approach is implemented by developing a complex S-function tool box in Simulink inside a MATLAB environment This choice has been made so as to synthesise the speed of S-function, the user friendliness of Simulink and the popularity of MATLAB.

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.

A voltage-sensorless control method to balance the input currents of a three-wire boost rectifier under unbalanced input voltages condition

This paper proposes a control method that can balance the input currents of the three-phase three-wire boost rectifier under unbalanced input voltage condition. The control objective is to operate the rectifier in the high-power-factor mode under balanced input voltage condition but to give overriding priority to the current balance function in case of unbalance in the input voltage. The control structure has been divided into two major functional blocks. The inner loop current-mode controller implements resistor emulation to achieve high-power-factor operation on each of the two orthogonal axes of the stationary reference frame. The outer control loop performs magnitude scaling and phase-shifting operations on current of one of the axes to make it balanced with the current on the other axis. The coefficients of scaling and shifting functions are determined by two closed-loop prportional-integral (PI) controllers that impose the conditions of input current balance as PI references. The control algorithm is simple and high performing. It does not require input voltage sensing and transformation of the control variables into a rotating reference frame. The simulation results on a MATLAB-SIMULINK platform validate the proposed control strategy. In implementation Texas Instrument's digital signal processor TMS320F24OF is used as the digital controller. The control algorithm for high-power-factor operation is tested on a prototype boost rectifier under nominal and unbalanced input voltage conditions.

Design, modelling and simulation of vibratory micromachined gyroscopes

Among various MEMS sensors, a rate gyroscope is one of the most complex sensors from the design point of view. The gyro normally consists of a proof mass suspended by an elaborate assembly of beams that allow the system to vibrate in two transverse modes. The structure is normally analysed and designed using commercial FEM packages such as ANSYS or MEMS specific commercial tools such as Coventor or Intellisuite. In either case, the complexity in analysis rises manyfolds when one considers the etch hole topography and the associated fluid flow calculation for damping. In most cases, the FEM analysis becomes prohibitive and one resorts to equivalent electrical circuit simulations using tools like SABER in Coventor. Here, we present a simplified lumped parameter model of the tuning fork gyro and show how easily it can be implemented using a generic tool like SIMULINK. The results obtained are compared with those obtained from more elaborate and intense simulations in Coventor. The comparison shows that lumped parameter SIMULINK model gives equally good results with fractional effort in modelling and computation. Next, the performance of a symmetric and decoupled vibratory gyroscope structure is also evaluated using this approach and a few modifications are made in this design to enhance the sensitivity of the device.

A current error space vector based hysteresis controller with constant switching frequency and simple online boundary computation for VSI fed IM drive

This paper proposes a simple current error space vector based hysteresis controller for two-level inverter fed Induction Motor (IM) drives. This proposed hysteresis controller retains all advantages of conventional current error space vector based hysteresis controllers like fast dynamic response, simple to implement, adjacent voltage vector switching etc. The additional advantage of this proposed hysteresis controller is that it gives a phase voltage frequency spectrum exactly similar to that of a constant switching frequency space vector pulse width modulated (SVPWM) inverter. In this proposed hysteresis controller the boundary is computed online using estimated stator voltages along alpha and beta axes thus completely eliminating look up tables used for obtaining parabolic hysteresis boundary proposed in. The estimation of stator voltage is carried out using current errors along alpha and beta axes and steady state model of induction motor. The proposed scheme is simple and capable of taking inverter upto six step mode operation, if demanded by drive system. The proposed hysteresis controller based inverter fed drive scheme is simulated extensively using SIMULINK toolbox of MATLAB for steady state and transient performance. The experimental verification for steady state performance of the proposed scheme is carried out on a 3.7kW IM.

Magnetic arm-switch-based three-phase series-shunt compensated quality AC power supply

This study presents a novel magnetic arm-switch-based integrated magnetic circuit for a three-phase series-shunt compensated uninterruptible power supply (UPS). The magnetic circuit acts as a common interacting field for a number of energy ports, viz., series inverter, shunt inverter, grid and load. The magnetic arm-switching technique ensures equivalent series or shunt connection between the inverters. In normal grid mode (stabiliser mode), the series inverter is used for series voltage correction and the shunt one for current correction. The inverters and the load are effectively connected in parallel when the grid power is not available. These inverters are then used to share the load power. The operation of the inverters in parallel is ensured by the magnetic arm-switching technique. This study also includes modelling of the magnetic circuit. A graphical technique called bond graph is used to model the system. In this model, the magnetic circuit is represented in terms of gyrator-capacitors. Therefore the model is also termed as gyrator-capacitor model. The model is used to extract the dynamic equations that are used to simulate the system using MATLAB/SIMULINK. This study also discusses a synchronously rotating reference frame-based control technique that is used for the control of the series and shunt inverters in different operating modes. Finally, the gyrator-capacitor model is validated by comparing the simulated and experimental results.

Common-mode voltage eliminated three-level inverter using a three-level flying-capacitor inverter and cascaded H-bridge

This paper proposes a new 3 level common mode voltage eliminated inverter using an inverter structure formed by cascading a H-Bridge with a three-level flying capacitor inverter. The three phase space vector polygon formed by this configuration and the polygon formed by the common-mode eliminated states have been discussed. The entire system is simulated in Simulink and the results are experimentally verified. This system has an advantage that if one of devices in the H-Bridge fails, the system can still be operated as a normal 3 level inverter mode at full power. This inverter has many advantages like use of single DC-supply, making it possible for a back to back grid-tied converter application, improved reliability etc.

A Three-Level Common-Mode Voltage Eliminated Inverter With Single DC Supply Using Flying Capacitor Inverter and Cascaded H-Bridge

A three-level common-mode voltage eliminated inverter with single dc supply using flying capacitor inverter and cascaded H-bridge has been proposed in this paper. The three phase space vector polygon formed by this configuration and the polygon formed by the common-mode eliminated states have been discussed. The entire system is simulated in Simulink and the results are experimentally verified. This system has an advantage that if one of devices in the H-bridge fails, the system can still be operated as a normal three-level inverter at full power. This inverter has many other advantages like use of single dc supply, making it possible for a back-to-back grid-tied converter application, improved reliability, etc.

Study on ride comfort assessment of multiple occupants using lumped parameter analysis

Growing consumer expectations continue to fuel further advancements in vehicle ride comfort analysis including development of a comprehensive tool capable of aiding the understanding of ride comfort. To date, most of the work on biodynamic responses of human body in the context of ride comfort mainly concentrates on driver or a designated occupant and therefore leaves the scope for further work on ride comfort analysis covering a larger number of occupants with detailed modeling of their body segments. In the present study, governing equations of a 13-DOF (degrees-of-freedom) lumped parameter model (LPM) of a full car with seats (7-DOF without seats) and a 7-DOF occupant model, a linear version of an earlier non-linear occupant model, are presented. One or more occupant models can be coupled with the vehicle model resulting into a maximum of 48-DOF LPM for a car with five occupants. These multi-occupant models can be formulated in a modular manner and solved efficiently using MATLAB/SIMULINK for a given transient road input. The vehicle model and the occupant model are independently verified by favorably comparing computed dynamic responses with published data. A number of cases with different dispositions of occupants in a small car are analyzed using the current modular approach thereby underscoring its potential for efficient ride quality assessment and design of suspension systems.

Active yaw control of a vehicle using a Fuzzy logic algorithm

Yaw rate of a vehicle is highly influenced by the lateral forces generated at the tire contact patch to attain the desired lateral acceleration, and/or by external disturbances resulting from factors such as crosswinds, flat tire or, split-μ braking. The presence of the latter and the insufficiency of the former may lead to undesired yaw motion of a vehicle. This paper proposes a steer-by-wire system based on fuzzy logic as yaw-stability controller for a four-wheeled road vehicle with active front steering. The dynamics governing the yaw behavior of the vehicle has been modeled in MATLAB/Simulink. The fuzzy controller receives the yaw rate error of the vehicle and the steering signal given by the driver as inputs and generates an additional steering angle as output which provides the corrective yaw moment. The results of simulations with various drive input signals show that the yaw stability controller using fuzzy logic proposed in the current study has a good performance in situations involving unexpected yaw motion. The yaw rate errors of a vehicle having the proposed controller are notably smaller than an uncontrolled vehicle's, and the vehicle having the yaw stability controller recovers lateral distance and desired yaw rate more quickly than the uncontrolled vehicle.

A 5th and 7th Order Harmonic Suppression Scheme for Open-end Winding Asymmetrical Six-phase IM Drive Using Capacitor-fed Inverter

Voltage source inverter (VSI) fed six-phase induction motor drives have high 6n +/- 1; n = odd order harmonic currents, due to absence of back emf for these currents. To suppress these harmonic currents, either bulky inductive harmonic filters or complex pulse width modulation (PWM) techniques have to be used. This paper proposes a simple harmonic elimination scheme using capacitor fed inverters, for an asymmetrical six-phase induction motor VSI fed drive. Two three phase inverters fed from a single capacitor is used on the open-end side of the motor, to suppress 6n +/- 1; n = odd order harmonics. A PWM scheme that can suppress the harmonics, as well as balance the capacitor voltage is also proposed. The capacitor fed inverters are switched so that the fundamental voltage is not affected. The proposed scheme is verified using MATLAB Simulink simulation at different speeds. The effectiveness of the scheme is demonstrated by comparing the results with those obtained by disabling the capacitor fed inverters. Experimental results are also provided to validate the functionality of the proposed controller.

On-line Estimation of Fundamental and Ripple Components of Line Currents in a Voltage-Source Inverter Operated at Low Switching Frequency

High-power voltage-source inverters (VSI) are often switched at low frequencies due to switching loss constraints. Numerous low-switching-frequency PWM techniques have been reported, which are quite successful in reducing the total harmonic distortion under open-loop conditions at such low operating frequencies. However, the line current still contains low-frequency components (though of reduced amplitudes), which are fed back to the current loop controller during closed-loop operation. Since the harmonic frequencies are quite low and are not much higher than the bandwidth of the current loop, these are amplified by the current controller, causing oscillations and instability. Hence, only the fundamental current should be fed back. Filtering out these harmonics from the measured current (before feeding back) leads to phase shift and attenuation of the fundamental component, while not eliminating the harmonics totally. This paper proposes a method for on-line extraction of the fundamental current in induction motor drives, modulated with low-switching-frequency PWM. The proposed method is validated through simulations on MATLAB/Simulink. Further, the proposed algorithm is implemented on Cyclone FPGA based controller board. Experimental results are presented for an R-L load.