Abstract Translation validation is an undecidable problem. Bisimulation relation based approaches, nevertheless, have been widely successful in translation validation of programs albeit with some drawbacks. These drawbacks include non-termination of the verification methodology and significant restrictions on the structures of programs to be checked for equivalence. We have developed a path based equivalence checker which propagates mismatched values over consecutive paths to alleviate these drawbacks. In this work, we show how a bisimulation relation between a program and its translated version can be constructed from the outputs of such a value propagation based equivalence checker. Moreover, none of the earlier methods that establish equivalence through construction of bisimulation relations has been shown to tackle code motions across loops; the present work demonstrates, for the first time, the existence of a bisimulation relation under such a situation.

Constructing bisimulation relations between programs as a means of translation validation has been an active field of study. The problem is in general undecidable. Currently available mechanisms suffer from drawbacks such as non-termination and significant restrictions on the structures of programs to be checked. We have developed a path extension based equivalence checking method as an alternative translation validation technique to alleviate these drawbacks. In this work, path extension based equivalence checking of programs (flowcharts) is leveraged to establish a bisimulation relation between a program and its translated version by constructing the relation from the outputs of the equivalence checker.

Compiler optimization of array-intensive programs involves extensive application of loop transformations and arithmetic transformations. Hence, translation validation of array-intensive programs requires manipulation of intervals of integers (representing domains of array indices) and relations over such intervals to account for loop transformations and simplification of arithmetic expressions to handle arithmetic transformations. A major obstacle for verification of such programs is posed by the presence of recurrences, whereby an element of an array gets defined in a statement S inside a loop in terms of some other element(s) of the same array which have been previously defined through the same statement S. Recurrences lead to cycles in the data-dependence graph of a program which make dependence analyses and simplifications (through closed-form representations) of the data transformations difficult. Another technique which works better for recurrences does not handle arithmetic transformations. In this work, array data-dependence graphs (ADDGs) are used to represent both the original and the optimized versions of the program and a validation scheme is proposed where the cycles due to recurrences in the ADDGs are suitably abstracted as acyclic subgraphs. Thus, this work provides a unified equivalence checking framework to handle loop and arithmetic transformations along with most of the recurrences -- this combination of features had not been achieved by a single verification technique earlier.

The initial behavioural specification of any software programs goes through significant optimizing and parallelizing transformations, automated and also human guided, before being mapped to an architecture. Establishing validity of these transformations is crucial to ensure that they preserve the original behaviour. PRES+ model (Petri net based Representation of Embedded Systems) encompassing data processing is used to model parallel behaviours. Being value based with inherent scope of capturing parallelism, PRES+ models depict such data dependencies more directly; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential variable-based IRs like Finite State Machines with Data path (FSMDs) (which are essentially sequential control flow graphs (CFGs)). In this work, a path based equivalence checking method for PRES+ models is presented.

A compiler is a computer program which translates a source code into a target code, often with an objective to reduce the execution time and/or save critical resources. However, an error in the design or in the implementation of a compiler may result in software bugs in the target code obtained from that compiler. Translation validation is a formal verification approach for compilers whereby, each individual translation is followed by a validation phase which verifies that the target code produced correctly implements the source code. In this paper, we present a tool for translation validation of optimizing transformations of programs; the original and the transformed programs are modeled as Finite State Machines with Datapath having Arrays (FSMDAs) and a symbolic value propagation (SVP) based equivalence checking strategy is applied over this model to determine the correctness of the applied transformations. The tool has been demonstrated to handle uniform and non-uniform code motions, including code motions across loops, along with transformations which result in modification of control structures of programs. Moreover, arithmetic transformations such as, associative, commutative, distributive transformations, expression simplification, constant folding, etc., are also supported.

Execution of cryptographic algorithm in hardware or software usually leaves power/current traces that are dependent on the data being processed. Power analysis attacks (PAAs) have been found to be extremely effective on such systems to derive the cryptographic secrets from these traces. Therefore, countering PAAs is of great importance. In this work, a Binary Decision Diagram (BDD) based dual-rail logic circuit scheme has been developed to counter PAAs. This circuit scheme features novel pre-charge generation, voltage scaling with leakage power minimization and early propagation effect resistance mechanism. A simple synthesis algorithm for mapping given Boolean functions to such BDD based circuits is also presented. The synthesized circuits feature low power circuitry and extremely low peak power variation. Experimental results for elementary gates such as AND, OR, NOT, XOR, NAND, NOR and the Lucifer and the Present S-boxes highlight the advantages of circuits based on this scheme with respect to peak power variance, average power and average current when compared with two other techniques - DP-BDD and SDMLp. Resistance of our S-box implementations to strong differential power analysis and correlation power analysis attacks have also been experimentally demonstrated. All results have been obtained using 65nm technology.

An equivalence checking method of finite state machines with datapath based on value propagation over model paths is presented here for validation of code motion transformations commonly applied during the scheduling phase of high-level synthesis. Unlike many other reported techniques, the method is able to handle code motions across loop bodies. It consists in propagating the variable values over a path to the subsequent paths on discovery of mismatch in the values for some live variable, until the values match or the final path segments are accounted for without finding a match. Checking loop invariance of the values being propagated beyond the loops has been identified to play an important role. Along with uniform and nonuniform code motions, the method is capable of handling control structure modifications as well. The complexity analysis depicts identical worst case performance as that of a related earlier method of path extension which fails to handle code motion across loops. The method has been implemented and satisfactorily tested on the outputs of a basic block-based scheduler, a path-based scheduler, and the high-level synthesis tool SPARK for some benchmark examples.

The finite state machine with datapath (FSMD) models provide a formalism to represent any sequential behavior. Literature has many examples where this model has been successfully applied for behavioral verification of programs. All these methods, however, cannot handle an important class of programs, namely those involving arrays. This limitation is now overcome with finite state machine with datapath having arrays (FSMDA) models which are an extension of FSMD models; the corresponding equivalence checking algorithm has also been enhanced so that code motions of array-intensive behaviors can be validated. The new mechanism has been successfully tested with several examples.

Differential power analysis (DPA) attacks are the most powerful side channel attacks against cryptographic systems. In this work, a reduced ordered binary decision diagram (ROBDD) based dual rail circuit for a basic DPA resistant cell has been designed. The specialty of this cell is that the overall input current of the cell is invariant to the input combinations of data bits applied to the cell. For the first time, bottom pre-charge logic is used in the design of such a cell. The ROBDD based design minimizes both area and early propagation effect. A number of logic functions including AND, OR, XOR, NOT, NAND, NOR and also an adder, all based on the basic cell, have then been designed in a hierarchical manner. Experimental results demonstrate DPA resistance of the circuits (for example an adder) developed using this cell, outperforming other competing design with respect to peak power variance.

Loop transformation techniques along with arithmetic transformations are applied extensively on array and loop intensive behaviors in design of area/energy efficient systems in the domain of multimedia and signal processing applications. Ensuring correctness of such transformations is crucial for the reliability of the designed systems. In this paper, array data dependence graphs (ADDGs) are used to represent both the input and the transformed behaviors and the correctness of the transformations is ensured by proving equivalence of the two ADDGs. A slice-based equivalence checking method of ADDGs is proposed for this purpose. The method relies on the normalization of arithmetic expressions and some simplification rules to handle arithmetic transformations. Unlike many other reported techniques, our method is strong enough to handle several arithmetic transformations along with all kinds of loop transformations. Correctness and complexity of the method have been dealt with. Experimental results on several test cases demonstrate the effectiveness of the method.

A formal verification method for checking correctness of code motion techniques is presented in this article. Finite State Machine with Datapath (FSMD) models have been used to represent the input and the output behaviors of each synthesis step. The method introduces cutpoints in one FSMD, visualizes its computations as concatenation of paths from cutpoints to cutpoints, and then identifies equivalent finite path segments in the other FSMD; the process is then repeated with the FSMDs interchanged. Unlike many other reported techniques, the method is capable of verifying both uniform and nonuniform code motion techniques. It has been underlined in this work that for nonuniform code motions, identifying equivalent path segments involves model checking of some data-flow properties. Our method automatically identifies the situations where such properties are needed to be checked during equivalence checking, generates the appropriate properties, and invokes the model checking tool NuSMV to verify them. The correctness and the complexity of the method have been dealt with. Experimental results demonstrate the effectiveness of the method.

A minimum connected dominating set (MCDS) offers an optimized way of sending messages in wireless networks. However, constructing a MCDS is a NP-complete problem. Many heuristics based approximation algorithms for MCDS problems have been previously reported. In this paper, we propose a new degree-based multiple leaders initiated greedy approximation algorithm (PSCASTS) based on the selection of a pseudo-dominating set and an improved Steiner tree construction. We also show that our PSCASTS outperforms existing CDS construction algorithms in terms of CDS size and construction costs. The simulation results show that PSCASTS constructs better non-trivial CDSs for networks with uniform, nearly-uniform and random distribution of sensor nodes. While PSCASTS retains the current best performance ratio of (4.8+ln5)|opt|+1.2, |opt| being the size of an optimal CDS of the network, it has the best time complexity of O(D), where D is the network diameter.

A formal verification method of the datapath and controller generation phase of a high-level synthesis (HLS) process is described in this paper. The goal is achieved in two steps. In the first step, the datapath interconnection and the controller finite state machine description generated by a high-level synthesis process are analyzed to obtain the register transfer-operations executed in the datapath for a given control assertion pattern in each control step. In the second step, an equivalence checking method is deployed to establish equivalence between the input and the output behaviors of this phase. A rewriting method has been developed for the first step. Unlike many other reported techniques, our method is capable of validating pipelined and multicycle operations, if any, spanning over several states. The correctness and complexity of the presented method have been treated formally. The method is implemented and integrated with an existing HLS tool, called structured architecture synthesis tool. The experimental results on several HLS benchmarks indicate the effectiveness of the presented method.

A minimum connected dominating set (MCDS) is used as virtual backbone for efficient routing and broadcasting in ad hoc sensor networks. The minimum CDS problem is NP-complete even in unit disk graphs. Many heuristics-based distributed approximation algorithms for MCDS problems are reported and the best known performance ratio has (4.8 + 1n 5). We propose a new heuristic called collaborative cover using two principles: 1) domatic number of a connected graph is at least two and 2) optimal substructure defined as subset of independent dominator preferably with a common connector. We obtain a partial Steiner tree during the construction of the independent set (dominators). A final postprocessing step identifies the Steiner nodes in the formation of Steiner tree for the independent set of G. We show that our collaborative cover heuristics are better than degree-based heuristics in identifying independent set and Steiner tree. While our distributed approximation CDS algorithm achieves the performance ratio of (4.8 + 1n 5) opt + 1.2, where opt is the size of any optimal CDS, we also show that the collaborative cover heuristic is able to give a marginally better bound when the distribution of sensor nodes is uniform permitting identification of the optimal substructures. We show that the message complexity of our algorithm is O(n¿2), ¿ being the maximum degree of a node in graph and the time complexity is O(n).

The mobility of nodes with a purpose called as robotic-mobility is used for replenishing energy to strategic military applications. Connected dominating set(CDS) provides a virtual backbone in adhoc network. Assuming a CDS based backbone in place, we give a technique of maintaining the location of mobile node for a given topology setting. We show that using a weighted CDS reduces the maintenance of location updates for mobile node. The complexity of our mobile-node maintanence algorithm is at most O(d. log d) where d is number of boundary crossings in the single node's movement. The simulation shows that our weighted CDS method for mobile-nodes achieve 40\% reduction in location maintenance using to shortest-hop path in CDS.

Wireless ad hoc and sensor networks (WSNs) often require a connected dominating set (CDS) as the underlying virtual backbone for efficient routing. Nodes in a CDS have extra computation and communication load for their role as dominator, subjecting them to an early exhaustion of their battery. A simple mechanism to address this problem is to switch from one CDS to another fresh CDS, rotating the active CDS through a disjoint set of CDSs. This gives rise to the connected domatic partition (CDP) problem, which essentially involves partitioning the nodes V(G) of a graph G into node disjoint CDSs. We have developed a distributed algorithm for constructing the CDP using our maximal independent set (MlS)-based proximity heuristics, which depends only on connectivity information and does not rely on geographic or geometric information. We show that the size of a CDP that is identified by our algorithm is at least [delta+1/beta(c+1)] - f, where delta is the minimum node degree of G, beta les 2, c les 11 is a constant for a unit disk graph (UDG), and the expected value of f is epsidelta|V|, where epsi Lt 1 is a positive constant, and delta ges 48. Results of varied testing of our algorithm are positive even for a network of a large number of sensor nodes. Our scheme also performs better than other related techniques such as the ID-based scheme.

Abstract Nodes in wireless sensor networks (WSN) are deployed in an unattended environment with non re‐chargeable batteries. Thus, energy efficiency becomes a major design goals in WSNs. Clustering becomes an effective technique for optimization energy in various applications like data gathering. Although aggregation aware clustering addresses lifetime and scalability goals, but suffers from excessive energy overhead at clusterhead nodes. Load balancing in existing clustering schemes often use rotation of clusterhead roles among all nodes in order to prevent any single node from complete energy exhaustion. We considered important aspects of energy and time overhead in rotation of the clusterhead roles in various node clustering algorithms with goals to further prolong the network lifetime by minimizing the energy overheads in rotation setup. The problem of clusterhead rotation is abstracted as the graph‐theoretic problem of domatic partitioning, which is also NP‐complete. The dense deployment and unattended nature rules out the possibility of manual or external control in existing domatic partition (DP) techniques to be used for WSNs. To our knowledge, no self‐organizing technique exists for domatic partitioning. We developed a distributed self‐organizing one‐domatic partitioning scheme with approximation factor of at least 1/16 for unit‐disk‐graphs (UDGs). In this work, we demonstrate that the benefits of self‐organization is achieved without sacrificing the quality of domatic partitioning. We demonstrated through simulations that our self‐organizing DP without sacrificing on the size of DP achieves self‐organization capability which is able to reduce time and energy overheads of clusterhead rotation resulting to an improved network lifetime compared to the existing clustering protocols for sensor networks. Copyright © 2008 John Wiley & Sons, Ltd.

A formal method for checking equivalence between a given behavioral specification prior to scheduling and the one produced by the scheduler is described. Finite state machine with data path (FSMD) models have been used to represent both the behaviors. The method consists of introducing cutpoints in one FSMD, visualizing its computations as concatenation of paths from cutpoints to cutpoints, and identifying equivalent finite path segments in the other FSMD; the process is then repeated with the FSMDs interchanged. Unlike many other reported techniques, this method is strong enough to work when path segments in the original behavior are merged, a common feature of scheduling. It is also capable of verifying several arithmetic transformations and many code-motion techniques employed during scheduling. Correctness and complexity of the method have been dealt with. Experimental results for several high-level synthesis benchmarks demonstrate the effectiveness of the method.

This paper presents an exploration procedure for mapping given functional specifications of an analog system to the specification parameters of individual component blocks of the system topology. A meet-in-the-middle approach has been followed for constructing the feasible design space. It is constructed as the intersection of an application-bounded specification space and a circuit-realizable specification space. The least squares support vector machine principle is used to accurately identify the actual geometry of the feasible design space. The reduced design space speeds up the exploration procedure. The benefit of our methodology is the ability to obtain practically correct circuit-level specifications of the component blocks of the system in a single pass. The effectiveness of the procedure has been demonstrated by considering a complete system. The simulation results satisfy the desired specifications of the system, validating the overall procedure.

This paper describes a formal verification methodology of high-level synthesis (HLS) process. The abstraction level of the input to HLS is so high compared to thatof the output that the verification has to proceed hand-in-hand with the synthesis process. The HLS verificationis performed in three phases in this work. The verification method is based on equivalence checking of two finite state machines with data-paths(FSMDs). Unlike most reported works that targets the individual phases independently, the proposed method applies to all these three phases. The method is strong enoughto accommodate control structure modification of the original behaviour, application of several code motion techniques during scheduling and register optimization during register allocation. It can also verify the correctness of the controller. A hand-in-hand synthesis and verification tool SAST has been developed and tested for effectiveness on several HLS benchmark circuits.

The sensitivity of the response of an analog system to circuit parameter variations is a vital performance metric for evaluation of its quality. This paper proposes a unified high level synthesis methodology for higher order continuous time state variable filters, considering the optimization of this metric. Minimization of the hardware count, which is another important issue, has also been taken into account at a much earlier stage of design. The entire methodology is illustrated with the case study of a state variable low pass filter and the benefits of the approach are clearly brought out.

This paper proposes a novel high level synthesis methodology for optimal linear analog systems in a formal and systematic way. It takes as an input, a high level description as well as the desired specifications of the system and gives as an output, an optimal sized architecture as well as certain constraints. This facilitates hierarchical analog system design and reduces circuit designers' effort by providing block level sizes with appropriate tolerance level. The methodology defines an abstract description of the system, selects an optimal architecture by exploring the entire architecture space and finally performs a behavioral sizing of the architecture. The entire methodology is illustrated with the case study of a state variable filter and the benefits of the approach are clearly brought out.

Present day designers require deep reasoning methods to analyze circuit timing. This includes analysis of effects of dynamic behavior (like glitches) on critical paths, simultaneous switching and identification of specific patterns and their timings. This paper proposes a novel approach that uses a combination of symbolic event propagation and temporal reasoning to extract timing properties of gate-level circuits. The formulation captures complex situations like triggering of traditional false paths and simultaneous switching in a unified symbolic representation in addition to identifying false paths, critical paths as well as conditions for such situations. This information is then represented as an event-time graph. A simple temporal logic on events is proposed that can be used to formulate a wide class of useful queries for various input scenarios. These include maximum/minimum delays, transition times, duration of patterns, etc. An algorithm is developed that retrieves answers to such queries from the event-time graph. A complete BDD based implementation of this system has been made. Results on the ISCAS85 benchmarks indicate very interesting properties of these circuits.

We present here a technique for allocation and binding for data path synthesis (DPS) using a Genetic Algorithm (GA) approach. This GA uses an unconventional crossover mechanism relying on a force directed data path binding completion algorithm. The data path is synthesized using some supplied design parameters. A bus-based interconnection scheme, use of multi-port memories, and provision for multicycling and pipelining are the main features of this system. The method presented here has been applied to standard benchmark examples and the results obtained are promising.

In this paper, we examine the multicriteria optimization involved in scheduling for data-path synthesis (DPS). The criteria we examine are the area cost of the components and schedule time. Scheduling for DPS is a well-known NP-complete problem. We present a method to find nondominated schedules using a combination of restricted search and heuristic scheduling techniques. Our method supports design with architectural constraints such as the total number of functional units, buses, etc. The schedules produced have been taken to completion using GABIND as written by Mandal et al., and the results are promising.