Author

Anmol Mathur

21 papers · 1996–2023

1996peak 5 in 19982023

Frequent co-authors

Papers

showing 1–21 of 21 RSS

Rate analysis for embedded systems

Anmol Mathur, Ali Dasdan, Rajesh K. Gupta

Hardware and Architecture · ACM Transactions on Design Automation of Electronic Systems · July 1998 · cited 59× · DOI ↗ · more like this ·

Embedded systems consist of interacting components that are required to deliver a specific functionality under constraints on execution rates and relative time separation of the components. In this article, we model an embedded system using concurrent processes interacting through synchronization. We assume that there are rate constraints on the execution rates of processes imposed by the designer or the environment of the system, where the execution rate of a process is the number of its executions per unit time. We address the problem of computing bounds on the execution rates of processes constituting an embedded system, and propose an interactive rate analysis framework. As part of the rate analysis framework we present an efficient algorithms for checking the consistency of the rate constraints. Bounds on the execution rate of each process are computed using an efficient algorithm…

Non-cycle-accurate sequential equivalence checking

Pankaj Chauhan, Deepak Goyal, Gagan Hasteer +2 more

Computational Theory and Mathematics · 26 Jul 2009 · cited 30× · DOI ↗ · more like this ·

We present a novel technique for Sequential Equivalence Checking (SEC) between non-cycle-accurate designs. The problem is routinely encountered in verifying the correctness of a system-level model versus an RTL design which has been derived from the former either manually or through high-level synthesis. The existing state-of-the-art in formal verification/SEC does not provide an efficient mechanism to perform such an equivalence check. Our technique reduces the SEC problem to a cycle-accurate equivalence-checking problem by constructing a pair of normalized cycle-accurate designs from the original designs, on which standard equivalence-checking techniques can then be deployed. We report the results of deploying our techniques on several industrial examples.

Functional Equivalence Verification Tools in High-Level Synthesis Flows

Anmol Mathur, Masahiro Fujita, E. M. Clarke +1 more

Computational Theory and Mathematics · IEEE Design & Test of Computers · July 2009 · cited 29× · DOI ↗ · more like this ·

Editor's note:High-level synthesis facilitates the use of formal verification methodologies that check the equivalence of the generated RTL model against the original source specification. The article provides an overview of sequential equivalence checking techniques, its challenges, and successes in real-world designs.—Andres Takach, Mentor Graphics

Embedded tutorial: Formal equivalence checking between system-level models and RTL

Alfred Koelbl, Yuan Lu, Anmol Mathur

Computational Theory and Mathematics · 2005 · cited 25× · OpenAlex ↗ · more like this ·

A rigorous system-level model (SLM) for a hardware design project is extremely important, often critical. Such a functional model not only defines the architect's ideas but also builds a precise foundation for both hardware designers and verification engineers. The key uses of SLMs are: architecture validation; performance modeling and architectural trade-off; platforms for software development and verification; and functional reference model. In this tutorial, we discuss how to formally verify sequential equivalence between SLMs and RTL, for both timed and untimed models. First, we provide a formal definition of the sequential equivalence. Then we discuss various formal verification technology that enables such practice in real designs.

Power Reduction Techniques and Flows at RTL and System Level

Anmol Mathur, Qi Wang

Hardware and Architecture · 2009 · cited 14× · DOI ↗ · more like this ·

Summary form only given. Power reduction is becoming a critical design criterion for ASIC/SOC designers. Reducing both dynamic and leakage power is imperative to meet power budgets for portable devices as well as to ensure that the systems that these ASICs meet their packaging and cooling costs. In addition, the power of an ASIC has a significant impact on its reliability and manufacturing yield. Traditionally, most automated power optimization tools have focused at gate-level and physical level optimizations. However, major power reductions are only possible by addressing power at the RTL and system levels. At these levels, it is possible to make the sequential modifications needed to reduce power and energy consumption via techniques like sequential clock gating, power gating, voltage/frequency scaling and other micro-architectural techniques. The focus of this tutorial will be on…

Improved merging of datapath operators using information content and required precision analysis

Anmol Mathur, Sanjeev Saluja

Hardware and Architecture · 2001 · cited 13× · DOI ↗ · more like this ·

Abstract: We introduce the notions of required precision and information content of datapath signals and use them to de ne functionally safe transformations on data ow graphs. These transformations reduce widths of datapath operators and enhance their mergeability. Using e cient algorithms to compute required precision and information content of signals, we de ne a new algorithm for partitioning a data ow graph consisting of datapath operators into mergeable clusters. Experimental results indicate that use of our clustering algorithm for operator merging based synthesis of datapath intensive designs, can lead to signi cant improvement in the delay and area of the implementation. 1.

RATAN: A Tool for Rate Analysis and Rate Constraint Debugging for Embedded Systems

Ali Dasdan, Anmol Mathur, Rajesh K. Gupta

Hardware and Architecture · 1997 · cited 10× · OpenAlex ↗ · more like this ·

The increasingly complex design of embedded systems creates the problems of specifying consistent and satisfiable rate constraints on process execution rates, checking them for consistency and satisfiability, computing process execution rates, and debugging rate constraint violations. The high complexity of these problems requires a complete and automated framework to help the designer in producing correct systems in shorter design time. We present such a framework and its implementation in a tool called Ratan. Experiments on large benchmarks show the suitability of the tool for an interactive debugging environment. 1 Introduction Embedded systems typically consist of several interacting processes that operate in parallel and execute at different rates. These processes are implemented in hardware as well as software. To ensure correct timing behavior and achieve performance goals…

Design for verification in system-level models and RTL

Anmol Mathur, Venkat Raghavan Krishnaswamy

Computational Theory and Mathematics · Proceedings - ACM IEEE Design Automation Conference · 2007 · cited 9× · DOI ↗ · more like this ·

It has long been the practice to create models in C or C++ for architectural studies, software prototyping and RTL verification in the design of Systems-on-Chip (SoC). It is often the case that by the end of a design project, multiple C models exist for different uses. Clearly, this leads to wasted effort on the part of model developers, and creates risk of functional divergence across models. In this paper we present some guidelines for system-level modeling and RTL design to allow for efficiently leveraging the system-level model for RTL verification via simulation based techniques, as well as via sequential equivalence checking. The paper presents the challenges of keeping system-level models and RTL synchronized from a functional perspective and presents some techniques for overcoming these challenges.

Efficient equivalence checking of multi-phase designs using retiming

Gagan Hasteer, Anmol Mathur, Prithviraj Banerjee

Computational Theory and Mathematics · 1998 · cited 7× · DOI ↗ · more like this ·

The use of multi-phase clocking scheme, aggressive pipelining and #sparse&quot; encodings in high performance designs results in a tremendous increase in the state space. In this paper, we show that automatically transforming such designs to ones that have more #dense&quot; encodings can result in signi#cant bene#ts in using implicit BDD-based techniques for their veri#cation. We formulate a relaxed retiming framework which is more powerful than traditional retiming in reducing the number of latches and show that it can be applied to the product machine model for checking sequential hardware equivalence #SHE# without altering the correctness of the SHE check. We combine retiming with phase abstraction #4# #a technique to transform multi-phase FSMs to single-phase FSMs for equivalence checking#. The two transformations enable the SHE check to be performed on high performance…

Generalized Kraft’s Inequality and Discrete<i>k</i>-Modal Search

Anmol Mathur, Edward M. Reingold

Artificial Intelligence · SIAM Journal on Computing · April 1996 · cited 7× · DOI ↗ · more like this ·

A function $f:\Re \to \Re $ is k-modal if its kth derivative has a unique zero. We study the problem of finding the smallest possible interval containing the unique zero of the kth derivative of such a function, assuming that the function is evaluated only at integer points. We present optimal algorithms for the case when k is even and for $k = 3$ and near-optimal algorithms when $k \geqslant 3$ and odd. A novel generalization of Kraft’s inequality is used to prove lower bounds on the number of function evaluations required. We show how our algorithms lead to an efficient divide-and-conquer algorithm to determine all turning points or zeros of a k-modal function. Unbounded k-modal search is introduced and some problems in extending previous approaches for unbounded searching to the k-modal case are discussed.

An implicit algorithm for finding steady states and its application to FSM verification

Gagan Hasteer, Anmol Mathur, Prithviraj Banerjee

Computational Theory and Mathematics · 1998 · cited 6× · DOI ↗ · more like this ·

Finding the set of steady states of a machine has applications in formal verification, sequential synthesis and ATPG. Existing techniques assume the presence of a designated set of initial states which is impractical in a real design environment. The set of steady state of a design is defined by the terminally strongly connected components (tSCCs) of the underlying state transition graph (STG). We show that multiple tSCCs and non-terminal SCCs need to be handled in a real design environment especially for verification. We present a fully implicit algorithm to find the steady states of a machine without any knowledge of initial states. We demonstrate the utility of our algorithm by applying it to FSM equivalence checking.

Efficient equivalence checking of multi-phase designs using phase abstraction and retiming

Gagan Hasteer, Anmol Mathur, P. Bannerjee

Hardware and Architecture · ACM Transactions on Design Automation of Electronic Systems · October 1998 · cited 3× · DOI ↗ · more like this ·

Equivalence checking of finite state machines (FSMs) traditionally assumes single phase machines where a single clock (implicit or explicit) synchronizes the state of the FSM. We extend the equivalence checking paradignm to FSMs with multi-phase clocks. Such designs are becoming increasingly popular in high performance microprocessors since they result in lower synchronization overhead. In addition, aggressive pipelining and the use of “sparse” encodings results in designs where the ratio of steady states to the total state space is very low. In this paper, we show that automatically transforming such designs to ones that have more “dense” encodings can result in significant benefits in using implicit BDD-based techniques for their verification. We explore two such techniques: phase abstraction and retiming and demonstrate their utility in the context of FSM equivalence checking. The…

HDL generation from parameterized schematic design system

Anmol Mathur, Pratiksh Vasant Parikh, Alan Mujumdar +5 more

Hardware and Architecture · 22 Nov 2002 · cited 2× · DOI ↗ · more like this ·

This paper presents an HDL generation method for generating synthesizable Verilog and VHDL models for DSP designs captured using a block-based schematic system. The schematic library consists of parameterized blocks that model various algorithmic functions. A schematic description of a design is first mapped to an HDL (Hardware Description Language) description, which is then synthesized using an RTL (Register-Transfer Level) or a behavioral synthesis tool. The HDL description generated by this method is optimized, easy-to-read and suited for RTL and behavioral synthesis tools. The synthesis results presented for some examples demonstrate the advantages of this technique.

An efficient assertion checker for combinational properties

Gagan Hasteer, Anmol Mathur, Prithviraj Banerjee

Computational Theory and Mathematics · 1997 · cited 2× · DOI ↗ · more like this ·

Formally verifying properties of signals in a circuit hasseveral applications in an equivalence checking based formalverification flow.In a hierarchical design, functionalityis divided across blocks.This necessitates the useof constraints on input signals of a block to avoid falsenegatives.Validating such input constraints requires assertionchecking at the outputs of modules generatingthe constrained signals.In this paper, we present anefficient assertion checker for combinational propertieswhich avoids the BDD explosion problem by finding anoptimal intermediate correlation free frontier.It hasbeen successfully used in an industrial setting to uncovera number of bugs.

PRELIMINARY REPORT OF A MODULAR INTERVENTION GUIDED BY FUNCTIONAL ANALYSIS FOR DEMENTIA CAREGIVERS

Subharati Ghosh, Benjamin D. Capistrant, Greta Friedemann‐Sánchez +4 more

Sociology and Political Science · The Gerontologist · 23 Oct 2015 · cited 1× · DOI ↗ · more like this ·

India's rapid demographic transitions -declining fertility, changing family structure, expansion of morbidity from complex, chronic diseases and increased life-expectancy -results in more elderly care falling on fewer family members. There remain critical gaps on: 1. how distribution of care roles and responsibilities vary by family structure, 2. the specific caregiving activities, and 3. how caregiving is conceptualized in the context of India. We conducted 30 semi-structured indepth interviews of older adults' caregivers identified by key informants in Jodhpur city, Rajasthan, and were sampled purposively, stratified by care recipient's condition (cognitive impairment, physical health condition, healthy/"normal" aging). Deductive data analysis was conducted based on care demands and caregiving role and responsibilities. Inductive analysis was conducted based on new themes that emerged…

Sequential equivalence checking

Anmol Mathur, Masahiro Fujita, S. Balakrishnan +1 more

Hardware and Architecture · 2006 · cited 1× · DOI ↗ · more like this ·

Summary form only for tutorial. We define sequential equivalence checking (SEC) to be the process of checking functional equivalence between models that do not satisfy the assumption of one-to-one flop mapping. The need for SEC is being driven by the widespread use of system-level modeling in SystemC/C/C++ for developing golden functional reference models, models for micro-architectural refinement and platforms for software development. This tutorial identifies the design flows where SEC can be effectively used, identify the key technologies needed for developing an effective SEC tool and demonstrate its value proposition in design flows.

Study of the Characteristics of Positive Contacts and Hospitalized Cases in Multiple Waves of the Covid -19 Pandemic in Pali District of Western Rajasthan: A Secondary Data Analysis

Subhash Gaur, Sinha Ln, Rajiv Agarwal +4 more

Modeling and Simulation · Indian Journal of Public Health Research & Development · 26 Sep 2023 · cited 0× · DOI ↗ · more like this ·

Background: Coronavirus disease 2019 (COVID-19), the pandemic that invaded the world in 2020, caused morethan 70 million cases and exceeded a million and a half deaths worldwide by the end of the year. Age and sex havebeen identified as two of the prominent risk factors in COVID-19 deaths. Early epidemiological studies conductedin China, India, and Iran revealed that fewer females were infected by SARS-CoV2(4-9).It is imperative for national governments to identify which population members are at high risk of becoming illor more likely to die. This analysis emphasizes the early epidemiological features of COVID-19 cases in the OPDin order to guide to policy decisions on the health, commercial, social, and economic fronts in case of any futuresurge in Covid cases.Methods: The data collected during contact tracing (urban and rural ) and hospital admissions during the periods:February 2020…

General Terms Verification, Algorithms

Pankaj Chauhan, Deepak Goyal, Gagan Hasteer +2 more

Urban Studies · 3 Sep 2016 · cited 0× · OpenAlex ↗ · more like this ·

We present a novel technique for Sequential Equivalence Checking (SEC) between non-cycle-accurate designs. The problem is rou-tinely encountered in verifying the correctness of a system-level model versus an RTL design which has been derived from the for-mer either manually or through high-level synthesis. The existing state-of-the-art in formal verification/SEC does not provide an effi-cient mechanism to perform such an equivalence check. Our tech-nique reduces the SEC problem to a cycle-accurate equivalence-checking problem by constructing a pair of normalized cycle-accurate designs from the original designs, on which standard equivalence-checking techniques can then be deployed. We report the results of deploying our techniques on several industrial examples.

Tutorial T7 Sequential Equivalence Checking

Anmol Mathur, S. Balakrishnan, Raj S. Mitra

Computational Theory and Mathematics · 2006 · cited 0× · OpenAlex ↗ · more like this ·

Traditional equivalence checkers used for RTL-to-gate-level equivalence rely on the exact matching of state points to reduce the problem of proving equivalence between the two models to that of proving equivalence between the next state functions of the corresponding state points and the functions at corresponding outputs. They are hence classified as combinational equivalence checkers. The need for proving equivalence between models that do not have exact one-to-one mapping between state points (flops/latches) has grown tremendously in the last few years. There are two main application domains that are driving the need for more powerful equivalence checking paradigms that relax the restriction on the exact matching of state points between the specification and the implementation: • System-level to RTL equivalence checking • RTL to RTL equivalence checking with sequential…

An implicit algorithm for finding steady states and its applications to FSM verifcation

Gagan Hasteer, Anmol Mathur, Prithviraj Banerjee

Computational Theory and Mathematics · 1998 · cited 0× · OpenAlex ↗ · more like this ·

Finding the set of steady states of a machine has applications in formal veri cation, sequential synthesis and ATPG. Existing techniques assume the presence of a designated set of initial states which is impractical in a real design environment. The set of steady states of a design is de ned by the terminally strongly connectedcomponents (tSCCs) of the underlying state transition graph (STG). We show that multiple tSCCs and non-terminal SCCs need tobe handledinareal design environment especially for veri cation. We present a fully implicit algorithm to nd the steady states of a machine without any knowledge of initial states. We demonstrate the utility of our algorithm by applying it to FSM equivalence checking. 1

RATAN: A Tool for Rate Analysis and Rate Constraint Debugging for. . .

Ali Dasdan, Anmol Mathur, Rajesh K. Gupta

Sociology and Political Science · 1997 · cited 0× · OpenAlex ↗ · more like this ·