Demo Data from EDBT 2026 / reviewers in the wild / expert
Mohamed H. Zaki
dblp:24/1409
· DBLP profile ↗
27ranked-venue papers
3as first author
2since 2021 · last 2022
0000-0002-2970-2423ORCID · conflict
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 20 · 1 first-author · 1 since 2021Software engineering, systems software and programming languages · 9 · 1 first-authorArtificial intelligence and machine learning · 2 · 1 since 2021Theory of computation · 2 · 1 first-authorApplied, interdisciplinary, general and emerging computing · 1 · 1 first-author
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Computer architecture, parallel and distributed computing, and storage systems
3 papers |
Electronic design automation · 69% Integrated circuit design · 31% |
Topics — the 6 heaviest of 6, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Electronic design automation › yield analysis
parametric yield estimation |
0.8 | 2 | 2020 | Mating Sensitivity Analysis and Statistical Verification for Efficient Yield Estimation · IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2020 Accelerated and Reliable Analog Circuits Yield Analysis Using SMT Solving Techniques · IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2018 |
Integrated circuit design
analog and mixed-signal circuits |
0.4 | 1 | 2020 | Mating Sensitivity Analysis and Statistical Verification for Efficient Yield Estimation · IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2020 |
Electronic design automation
yield analysis |
0.3 | 1 | 2018 | Accelerated and Reliable Analog Circuits Yield Analysis Using SMT Solving Techniques · IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2018 |
Integrated circuit design › analog and mixed-signal circuits
analog circuit design |
0.2 | 1 | 2015 | Towards enhancing analog circuits sizing using SMT-based techniques · DAC 2015 |
Electronic design automation › circuit sizing
analog circuit sizing |
0.2 | 1 | 2015 | Towards enhancing analog circuits sizing using SMT-based techniques · DAC 2015 |
Electronic design automation › circuit analysis
statistical circuit analysis |
0.1 | 1 | 2020 | Mating Sensitivity Analysis and Statistical Verification for Efficient Yield Estimation · IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2020 |
Methods — techniques the papers use, named apart from their topics
satisfiability modulo theories · 0.5statistical verification · 0.4sensitivity analysis · 0.4monte carlo simulation · 0.4hypothesis testing · 0.4statistical model checking · 0.3sparse regression · 0.3monte carlo · 0.3LASSO · 0.3
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2022 | An efficient hardware implementation of CNN-based object trackers for real-time applicationsabstractAbstract The object tracking field continues to evolve as an important application of computer vision. Real-time performance is typically required in most applications of object tracking. The recent introduction of Convolutional Neural network (CNN) techniques to the object tracking field enabled the attainment of significant performance gains. However, the heavy computational load required for CNNs conflicts with the real-time requirements required for object tracking. In this paper, we address these computational limitations on the algorithm-side and the circuit-side. On the algorithm side, we adopt interpolation schemes which can significantly reduce the processing time and the memory storage requirements. We also evaluate the approximation of the hardware-expensive computations to attain an efficient hardware design. Moreover, we modify the online-training scheme in order to achieve a constant processing time across all video frames. On the circuit side, we developed a hardware accelerator of the online training stage. We avoid transposed reading from the external memory to speed-up the data movement with no performance degradation. Our proposed hardware accelerator achieves 44 frames-per-second in training the fully connected layers. Al-Hussein A. El-Shafie, Mohamed H. Zaki, Serag El-Din Habib |
Neural Comput. Appl. | 2 |
| 2021 | Towards an Efficient Hardware Implementation of CNN-Based Object TrackersabstractConvolution Neural Network (CNN) has achieved a performance boost to the visual tracking field. However, CNN-based trackers feature slow computational speed and large memory size. These issues challenge the embedded implementation of the CNN-based trackers. In this paper, we show how interpolation schemes can significantly reduce the memory requirements. In addition, we present a design-space exploration of the fixed-point representation of the CNN-based trackers aiming for a cost-efficient hardware implementation. Moreover, we present a hardware accelerator of the online training stage of the tracker. Our proposed accelerator can train the whole fully connected layers at a rate of 45.9 frames-per-second. Al-Hussein A. El-Shafie, Mohamed H. Zaki, Serag El-Din Habib |
ISCAS | 2 |
| 2020 | Mating Sensitivity Analysis and Statistical Verification for Efficient Yield EstimationabstractParametric yield is a significant threat to the reliability of nanoscale analog and mixed-signal circuits. A critical yet challenging problem of yield estimation is to account for multiple circuit performance. In this paper, we propose a novel nonparametric statistical verification methodology to efficiently estimate the parametric yield due to 65-nm technology for multiperformance constraints. Our proposed approach exploits the fact that circuit parameters variation has different impacts on the circuit performance. Hence, a global sensitivity analysis classifies the circuit parameters according to their influence on the desired circuit performances. Based on this classification, an efficient joint recurrence verification (JRV) algorithm, a procedure inspired from DNA analysis, is performed on the most “critical/influential” parameters. A global hypothesis testing procedure is then performed based on the computed JRV metrics. We demonstrate the effectiveness of our methodology on two benchmark circuits. The acquired results show the ability of our approach to handle multiple corners and multiple performances yield problems with up to 11× speedup compared to conventional techniques with an average error smaller than 3%. Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2019 | Fast CNN-Based Object Tracking Using Localization Layers and Deep Features InterpolationabstractObject trackers based on Convolution Neural Network (CNN) have achieved state-of-the-art performance on recent tracking benchmarks, while they suffer from slow computational speed. The high computational load arises from the extraction of the feature maps of the candidate and training patches in every video frame. The candidate and training patches are typically placed randomly around the previous target location and the estimated target location respectively. In this paper, we propose novel schemes to speedup the processing of the CNN-based trackers. We input the whole region-of-interest once to the CNN to eliminate the redundant computations of the random candidate patches. In addition to classifying each candidate patch as an object or background, we adapt the CNN to classify the target location inside the object patches as a coarse localization step, and we employ bilinear interpolation for the CNN feature maps as a fine localization step. Moreover, bilinear interpolation is exploited to generate CNN feature maps of the training patches without actually forwarding the training patches through the network which achieves a significant reduction of the required computations. Our tracker does not rely on offline video training. It achieves competitive performance results on the OTB benchmark with 8x speed improvements compared to the equivalent tracker. Al-Hussein A. El-Shafie, Mohamed H. Zaki, Serag El-Din Habib |
IWCMC | 2 |
| 2018 | Accelerated and Reliable Analog Circuits Yield Analysis Using SMT Solving TechniquesabstractExisting yield analysis methods are computationally expensive and generally encounter challenges with high-dimensional process parameters space. In this paper, we propose a new method for accelerated and reliable computation of parametric yield that combines the advantages of sparse regression and satisfiability modulo theory (SMT) solving techniques, and avoids issues in both. The key idea is to characterize the failure regions as a collection of hyperrectangles in the parameters space. Toward this goal, the method constructs sparse polynomial models based on adaptive least absolute shrinkage and selection operator to find low degree approximations of the circuit performances. A procedure inspired by statistical model checking is then introduced to assess the model accuracy. Given the constructed models, an SMT-based solving algorithm is employed to locate the failure hyperrectangles in the parameters space. The yield estimation is based on a geometric calculation of probabilistic volumes subtended by the located hyperrectangles. We demonstrate the effectiveness of our method using circuits that require expensive run-time simulation during yield evaluation. They include: an integrated ring oscillator, a 6T static RAM cell and a multistage fully-differential amplifier. Experimental results show that the proposed method is suitable for handling problems with tens of process parameters. Meanwhile, it can provide 5×-2000× speed-up over Monte Carlo methods, when a high prediction accuracy is required. Ons Lahiouel, Mohamed H. Zaki, Sofiène Tahar |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2018 | Automated Analysis of Pedestrian Group Behavior in Urban SettingsabstractMovement trajectory of pedestrians, when tracked from video data, enables the automated analysis of individual's walking behavior. For example, speed preferences and walking strategies are typical behavior characteristics that benefit from this analysis. When pedestrians are walking in a group, they tend to adjust their speed and direction accordingly, while maintaining interpersonal distances. The adopted walking strategy leads to a coupling in their movement behavior. Such commonality, if considered, permits the discrimination between pedestrian groups and the distinction of pedestrians in different groups. Those are important factors when tracking a group of pedestrians or counting pedestrians in the crowd. The objective of this paper is localizing pedestrians in small groups using automated computer vision tracking. This paper describes the following tasks. First, to identify possible commonality in walking behavior between nearby pedestrians. This step is realized by proposing a new structural similarity measure of pedestrians' movement. Second, to provide a method for counting pedestrians in groups. A classification procedure accomplishes this task based on spatio-temporal criteria and the introduced movement similarity measure. Third, to show the feasibility of the method on a pedestrian group study from video data collected at a moderately dense pedestrian crosswalk in Vancouver, British Columbia. A validation of the group size classification demonstrated an accuracy of up to 77%. This paper enables a faster stream for comprehensive pedestrian data collection. Also, the new measure for group behavior can be useful when studying the mechanism of group formation and collision avoidance. Mohamed H. Zaki, Tarek Sayed |
IEEE Trans. Intell. Transp. Syst. | 1 |
| 2017 | Enhancing analog yield optimization for variation-aware circuits sizingabstractThis paper presents a novel approach for improving automated analog yield optimization using a two step exploration strategy. First, a global optimization phase relies on a modified Lipschitizian optimization to sample the potential optimal sub-regions of the feasible design space. The search locates a design point near the optimal solution that is used as a starting point by a local optimization phase. The local search constructs linear interpolating surrogate models of the yield to explore the basin of convergence and to rapidly reach the global optimum. Experimental results show that our approach locates higher quality design points in terms of yield rate within less run time and without affecting the accuracy. Ons Lahiouel, Mohamed H. Zaki, Sofiène Tahar |
DATE | 2 |
| 2017 | Exploiting bounds optimization for the semi-formal verification of analog circuits
Ons Lahiouel, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar |
Integr. | 3 |
| 2016 | Cross recurrence verification technique for process variation-resilient analog circuitsabstractThis paper explores the impact of device process variations on the performance of analog circuits. We propose a new verification approach called Cross Recurrence Verification (CRV). Circuit output similarities between an ideal circuit that has parameters set to the nominal values and a non-ideal circuit with process variation due to 65nm fabrication process are computed. CRV is used to find the percentage of recurrence and the longest common output subsequence that matches the output subsequence of an ideal circuit. The performed analysis showed the potential of this novel technique to enhance/improve the verification process of Analog circuits. The proposed approach is illustrated on a five stage ring oscillator. The obtained results demonstrate the robustness, accuracy and flexibility of our methodology. Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar |
ISCAS | 2 |
| 2016 | Enhancing Model Order Reduction for Nonlinear Analog Circuit SimulationabstractTraditionally, model order reduction methods have been used to reduce the computational complexity of mathematical models of dynamic systems, while preserving their functional characteristics. This technique can also be used to fasten analog circuit simulations without sacrificing their highly nonlinear behavior. In this paper, we present an iterative approach for reducing the computational complexity of nonlinear analog circuits using piecewise linear approximations,k-means clustering, and Krylov space projection techniques. We model primary circuit inputs, design initial conditions, and circuit parameters as fuzzy variables with different distributions in qualitative simulations. We then iteratively fine-tune the reduced models until a model is achieved that meets a predefined performance and accuracy conformance criteria. We demonstrate the effectiveness of our method using several key nonlinear circuits: 1) a transmission line; 2) a ring oscillator; 3) a voltage controlled oscillator; 4) a phase-locked loop; and 5) an analog comparator circuit. Our experiments show that the reduced model simulations are fast and accurate compared with the existing techniques. Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar |
IEEE Trans. Very Large Scale Integr. Syst. | 2 |
| 2015 | Towards enhancing analog circuits sizing using SMT-based techniquesabstractThis paper presents an approach for enhancing analog circuit sizing using Satisfiability Modulo Theory (SMT). The circuit sizing problem is encoded using nonlinear constraints. An SMT-based algorithm exhaustively explores the design space, where the biasing-level design variables are conservatively tracked using a collection of hyperrectangles. The device dimensions are then determined by accurately relating biasing to geometry-level design parameters. We demonstrate the feasibility and efficiency of the proposed methodology on a two-stage amplifier and a folded cascode amplifier. Experimental results show that our approach can achieve higher quality in analog synthesis and unrivaled coverage of the design space. Ons Lahiouel, Mohamed H. Zaki, Sofiène Tahar |
DAC | 2 |
| 2015 | Statistically Validating the Impact of Process Variations on Analog and Mixed Signal DesignsabstractProcess variation presents a practical challenge on the performance of analog and mixed signal (AMS) circuits. This paper proposes a Monte Carlo-Jackknife (MC-JK) technique, a variant of Monte Carlo method, to verify process variation affecting the performance and functionality of AMS designs. We use a behavioral model to which we encompass device variation due to $65nm$ technology process. Next, we conduct hypothesis testing based on the MC-JK technique combined with Latin hypercube sampling in a statistical run-time verification environment. Experimental results demonstrate the robustness of our approach in verifying AMS circuits. Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar |
ACM Great Lakes Symposium on VLSI | 2 |
| 2014 | A semi-formal approach for analog circuits behavioral properties verificationabstractWe propose an environment for the verification of analog circuits behavioral properties, where the circuit state space bounds are first computed using qualitative simulation. Then, their specified behavioral properties are verified on these bounds. The effectiveness of the method is illustrated with a tunnel diode oscillator. Ons Lahiouel, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar |
ACM Great Lakes Symposium on VLSI | 3 |
| 2014 | A qualitative simulation approach for verifying PLL locking propertyabstractSimulation cannot give a full coverage of Phase Locked Loop (PLL) behavior in presence of process variation, jitter and varying initial conditions. Qualitative Simulation is an attracting method that computes behavior envelopes for dynamical systems over continuous ranges of their parameters. Therefore, this method can be employed to verify PLLs locking property given a model that encompasses their imperfections. Extended System of Recurrence Equations (ESREs) offer a unified modeling language to model analog and digital PLLs components. In this paper, an ESRE model is created for both PLLs and their imperfections. Then, a modified qualitative simulation algorithm is used to guarantee that the PLL locking time is sound for every possible initial condition and parameter value. We used our approach to analyze a Charge Pump-PLL for a $0.18\mu m$ fabrication process and in the presence of jitter and initial conditions uncertainties. The obtained results show an improvement of simulation coverage by computing the minimum locking time and predicting a non locking case that statistical simulation technique fails to detect. Ibtissem Seghaier, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar |
ACM Great Lakes Symposium on VLSI | 3 |
| 2014 | Generation of reduced analog circuit models using transient simulation tracesabstractThe generation of fast models for device level circuit descriptions is a very active area of research. Model order reduction is an attractive technique for dynamical models size reduction. In this paper, we propose an approach based on clustering, curve-fitting, linearization and Krylov space projection to build reduced models for nonlinear analog circuits. We demonstrate our model order reduction method for three nonlinear circuits: a voltage controlled oscillator, an operational amplifier and a digital frequency divider. Our experimental results show that the reduced models lead to an improvement in simulation speed while guaranteeing the representation of the behavior of the original circuit design. Paul Winkler, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar |
ACM Great Lakes Symposium on VLSI | 3 |
| 2013 | Multiple Instance Learning by Discriminative Training of Markov Networks
Hossein Hajimirsadeghi, Jinling Li, Greg Mori, Mohamed H. Zaki, Tarek Sayed |
UAI | 4 |
| 2013 | Statistical Run-Time Verification of Analog Circuits in Presence of Noise and Process VariationabstractNoise and process variation present a practical limit on the performance of analog circuits. This paper proposes a methodology for modeling and verification of analog designs in the presence of shot noise, thermal noise, and process variations. The idea is to use stochastic differential equations to model noise in additive and multiplicative form and then combine process variation due to 0.18 μm technology in a statistical run-time verification environment. The efficiency of Monte-Carlo and Bootstrap statistical techniques are compared for a Colpitts oscillator and a phase locked loop-based frequency synthesizer circuit. Rajeev Narayanan, Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2012 | Towards improving simulation of analog circuits using model order reductionabstractLarge analog circuit models are very expensive to evaluate and verify. New techniques are needed to shorten time-to-market and to reduce the cost of producing a correct analog integrated circuit. Model order reduction is an approach used to reduce the computational complexity of the mathematical model of a dynamical system, while capturing its main features. This technique can be used to reduce an analog circuit model while retaining its realistic behavior. In this paper, we present an approach to model order reduction of nonlinear analog circuits. We model the circuit using fuzzy differential equations and use qualitative simulation and K-means clustering to discretion efficiently its state space. Moreover, we use a conformance checking approach to refine model order reduction steps and guarantee simulation acceleration and accuracy. In order to illustrate the effectiveness of our method, we applied it to a transmission line with nonlinear diodes and a large nonlinear ring oscillator circuit. Experimental results show that our reduced models are more than one order of magnitude faster and accurate when compared to existing methods. Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar |
DATE | 2 |
| 2012 | Verifying jitter in an analog and mixed signal design using dynamic time warpingabstractWe present a variant of dynamic time warping (DTW) algorithm to verify jitter properties associated with an analog and mixed signal (AMS) design. First, the AMS design with stochastic jitter component is modeled using a system of difference equations for analog and digital parts and then evaluated in a MATLAB simulation environment. Second, MonteCarlo simulation is combined with DTW and hypothesis testing to determine the probability of acceptance/rejection of those simulation results. Our approach is illustrated on analyzing the jitter effect on the “lock-time” property of a phase locked loop (PLL) based frequency synthesizer. Rajeev Narayanan, Alaeddine Daghar, Mohamed H. Zaki, Sofiène Tahar |
DATE | 3 |
| 2011 | Ensuring correctness of analog circuits in presence of noise and process variations using pattern matchingabstractThis paper relies on the longest closest subsequence (LCSS), a variant of the longest common subsequence (LCS), to account for noise and process variations inherited by analog circuits. The idea is to use stochastic differential equations (SDE) to model the design and integrate device variation due to the 0.18μm fabrication process in a MATLAB simulation environment. LCSS is used to find the longest and closest subsequence that matches with the subsequence of an ideal circuit. We illustrate the proposed approach on a Colpitts oscillator circuit. Advantages of the proposed methods are robustness and flexibility to account for wide range of variations. Rajeev Narayanan, Mohamed H. Zaki, Sofiène Tahar |
DATE | 2 |
| 2010 | Formal verification of analog circuits in the presence of noise and process variationabstractWe model and verify analog designs in the presence of noise and process variation using an automated theorem prover, MetiTarski. Due to the statistical nature of noise, we propose to use stochastic differential equations (SDE) to model the designs. We find a closed form solution for the SDEs, then integrate the device variation due to the 0.18¿m fabrication process and verify properties using MetiTarski. We illustrate the proposed approach on an inverting Op-Amp Integrator and a Band-Gap reference bias circuit. Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiène Tahar, Lawrence C. Paulson |
DATE | 3 |
| 2010 | Using Stochastic Differential Equation for Verification of Noise in Analog/RF Circuits
Rajeev Narayanan, Mohamed H. Zaki, Sofiène Tahar |
J. Electron. Test. | 2 |
| 2009 | Formal verification of analog designs using MetiTarskiabstractMetiTarski, an automatic theorem prover for inequalities on real-valued elementary functions, can be used to verify properties of analog circuits. First, a closed form solution to the model of the circuit is obtained. We present two techniques for obtaining the closed form solution. One is based on piecewise linear modeling and the inverse Laplace transform. The other is based on small-signal analysis and transfer function theory. Second, the properties of interest are turned into a set of inequalities involving analytic functions, which are proved automatically using MetiTarski. We verify properties concerning oscillation and the change in gain due to component tolerances. William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson |
FMCAD | 4 |
| 2007 | A symbolic methodology for the verification of analog and mixed signal designsabstractThe paper proposed a new symbolic verification methodology for proving the properties of analog and mixed signal (AMS) designs. Starting with an AMS description and a set of properties and using symbolic computation, a normal mathematical representation was extracted for the system in terms of recurrence equations. These normalized equations are used along with an induction verification strategy defined inside the computer algebra system Mathematica to prove the correctness of the properties. The methodology was applied on a third order DeltaSigma modulator Ghiath Al Sammane, Mohamed H. Zaki, Sofiène Tahar |
DATE | 2 |
| 2007 | Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL
Ghiath Al Sammane, Mohamed H. Zaki, Zhi Jie Dong, Sofiène Tahar |
FDL | 2 |
| 2007 | Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS DesignsabstractAnalog and mixed signal (AMS) designs are important integrated circuits that are usually needed at the interface between the electronic system and the real world. Recently, several formal techniques have been introduced for AMS verification. In this paper, we propose a difference equations based bounded model checking approach for AMS systems. We define model checking using a combined system of difference equations for both the analog and digital parts, where the state space exploration algorithm is handled with Taylor approximations over interval domains. We illustrate our approach on the verification of several AMS designs including \Delta \Sigma modulator and oscillator circuits. Mohamed H. Zaki, Ghiath Al Sammane, Sofiène Tahar, Guy Bois |
FMCAD | 1 |
| 2006 | A practical approach for monitoring analog circuitsabstractFormal methods have been advocated for the verification of digital design where correctness is proved mathematically. In contrast to digital designs, the verification of analog and mixed signal systems is a challenging task that requires lots of expertise and deep understanding of their behavior. In this paper, we present a run-time verification methodology based on monitoring the behavior (solution flow) of analog circuits. Monitors are deterministic timed automata that can be synthesized from temporal properties. For illustration purposes, we applied our methodology on the verification of the oscillation property of a tunnel diode oscillator. Mohamed H. Zaki, Sofiène Tahar, Guy Bois |
ACM Great Lakes Symposium on VLSI | 1 |