EDBT 2026 Demo / reviewers in the wild / expert
Alberto L. Sangiovanni-Vincentelli
dblp:s/ALSangiovanniV
· DBLP profile ↗
484ranked-venue papers
22as first author
29since 2021 · last 2026
0000-0003-1298-8389ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 340 · 17 first-author · 5 since 2021Software engineering, systems software and programming languages · 65 · 3 first-author · 7 since 2021Applied, interdisciplinary, general and emerging computing · 54 · 4 first-author · 3 since 2021Theory of computation · 33 · 2 first-author · 7 since 2021Artificial intelligence and machine learning · 21 · 11 since 2021Computer networks · 17 · 1 since 2021Graphics, computer vision, multimedia, augmented reality and games · 9 · 5 since 2021Databases, data management, data science and information retrieval · 2 · 1 since 2021Human-computer interaction and ubiquitous computing · 2
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | ScenicRules: An Autonomous Driving Benchmark with Multi-Objective Specifications and Abstract Scenarios
Kevin Kai-Chun Chang, Ekin Beyazit, Alberto L. Sangiovanni-Vincentelli, Tichakorn Wongpiromsarn, Sanjit A. Seshia |
IV | 3 |
| 2025 | Contract-based Component Selection Using BehaviorsabstractContract-based component selection reduces design time and cost by encouraging the reuse of subsystem designs from an existing library. However, existing techniques assume the objective function is expressed solely with component parameters, such as size, cost, and power consumed, adding the burden of characterizing components with parameters and deriving the appropriate objective as a function of these parameters. We argue that this process does not consider behavior abstractions that could make the selection process more effective. We propose a contract-based component selection algorithm that consists of two parts: a contract-based system reasoning part that guides the selection and a black-box optimizer that selects the final choice. The contract-based system-reasoning part can evaluate, verify, and suggest the selection based on system behavior using contract operations to guide the black-box optimizer. Experimental results based on the design problem for an unmanned aerial vehicle propulsion system, show that our proposed methods can successfully find and optimize component selection for all test cases within the time limit and outperform the existing methods. Sheng-Jung Yu, Alberto L. Sangiovanni-Vincentelli |
MEMOCODE | 2 |
| 2025 | Ensuring Strong Replaceability of Assume-guarantee Contract for Feedback CompositionabstractContract-based design is a promising design methodology that leverages rigorous specification, refinement relation, and composition operation for compositional reasoning to address system design complexity and heterogeneity by facilitating independent development of the subsystems. However, vacuous implementations—those with empty behaviors under the targeted environment—can occur even if the subsystem designers correctly refine the contracts according to the refinement relation. This compromises the benefits of independent development as vacuous implementations fail to satisfy the design goals. Although previous research emphasizes the importance of strong replaceability and receptiveness in addressing this issue, strong replaceability in feedback composition is not guaranteed. In this paper, we tackle this challenge by identifying conditions to ensure strong replaceability in feedback composition. These conditions are developed and validated through the analysis of fixed obligations, representing the behaviors collaboratively allowed by subsystem contracts, and fixed obligation graphs, which illustrate the relation between fixed obligations. We propose algorithms to verify strong replaceability for the subsystem contracts, offering a general approach that utilizes set operations and satisfiability modulo theories-based encoding to circumvent reliance on specific underlying theories in contract descriptions. By addressing this gap in contract-based design methodology, our developed conditions and algorithms ensure correct and meaningful implementations. Sheng-Jung Yu, Alberto L. Sangiovanni-Vincentelli |
MEMOCODE | 2 |
| 2025 | HypercontractsabstractAbstract Contract theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. This paper introduces hypercontracts , a compositional assume-guarantee formalism that supports the expression and manipulation of hyperproperties of arbitrary structure. Hyperproperties can express characteristics such as mean response times, security attributes, and robustness that lie outside the expressivity of trace properties and contracts. By considering hyperproperties with interval and downward closed structure, we obtain specializations of the theory of hypercontracts to interval and conic hypercontracts. These specializations are more general than assume-guarantee contracts but come with finite descriptions, while enabling new applications of contracts in security and autonomous cyber-physical system design. Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
Formal Methods Syst. Des. | 3 |
| 2025 | Correction: Hypercontracts
Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
Formal Methods Syst. Des. | 3 |
| 2025 | Model Residuals as Shields: A Two-Level Formulation to Defend Smart Grids From Poisoning AttacksabstractThe advancement of smart grids presents both vast opportunities and heightened cybersecurity risks. Data-driven defense mechanisms, though designed as a shield against these threats, can fall prey to poisoning attacks. We delve into regression settings, underscoring the imperative to fortify defenses against a spectrum of poison ratios, notably those above 0.5—an issue scarcely addressed in prior studies. Recognizing the susceptibilities of smart grids and their manipulable sensors, we exploit the very intent of poisoning attacks, compromising model accuracy, as our defense mechanism. Our proposed two-level optimization framework discerns between poisoned and authentic data based on model residuals, outperforming or matching existing methods in 72% to 77% of precision and 75% to 80% of recalls across various poisoning attacks, poison ratios, and datasets. Once the authentic data are identified, the trained model is adaptable for a variety of applications. Comprehensive evaluations on different smart grid datasets, pitted against myriad poisoning schemes, validate our methodology’s edge over existing methods. We also shed light on the implications of model misspecification originating from temporal auto-correlation, a common feature in IoT and smart grid data. Tung-Wei Lin, Padmaksha Roy, Yi Zeng 0005, Ming Jin 0002, Ruoxi Jia 0001, Chen-Ching Liu, Alberto L. Sangiovanni-Vincentelli |
IEEE Internet Things J. | 7 |
| 2025 | Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and DesignabstractContract-based design is a method to facilitate modular design of systems. While there has been substantial progress on the theory of contracts, there has been less progress on practical algorithms for the algebraic operations in the theory. In this article, we present (1) principles to implement a contract-based design tool at scale and (2) Pacti, a tool that can efficiently compute these operations. We illustrate the use of Pacti in a variety of case studies. Inigo Incer, Apurva Badithela, Josefine Graebener, Piergiuseppe Mallozzi, Ayush Pandey 0001, Nicolas Rouquette, Sheng-Jung Yu, Albert Benveniste, Benoît Caillaud, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
ACM Trans. Cyber Phys. Syst. | 11 |
| 2024 | Equivariant Ensembles and Regularization for Reinforcement Learning in Map-based Path PlanningabstractIn reinforcement learning (RL), exploiting environmental symmetries can significantly enhance efficiency, robustness, and performance. However, ensuring that the deep RL policy and value networks are respectively equivariant and invariant to exploit these symmetries is a substantial challenge. Related works try to design networks that are equivariant and invariant by construction, limiting them to a very restricted library of components, which in turn hampers the expressiveness of the networks. This paper proposes a method to construct equivariant policies and invariant value functions without specialized neural network components, which we term equivariant ensembles. We further add a regularization term for adding inductive bias during training. In a map-based path planning case study, we show how equivariant ensembles and regularization benefit sample efficiency and performance. Mirco Theile, Hongpeng Cao, Marco Caccamo, Alberto L. Sangiovanni-Vincentelli |
IROS | 4 |
| 2024 | Dynamic, Multi-objective Specification and Falsification of Autonomous CPS
Kevin Kai-Chun Chang, Kaifei Xu, Edward Kim 0005, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
RV | 4 |
| 2024 | Fear-Neuro-Inspired Reinforcement Learning for Safe Autonomous DrivingabstractEnsuring safety and achieving human-level driving performance remain challenges for autonomous vehicles, especially in safety-critical situations. As a key component of artificial intelligence, reinforcement learning is promising and has shown great potential in many complex tasks; however, its lack of safety guarantees limits its real-world applicability. Hence, further advancing reinforcement learning, especially from the safety perspective, is of great importance for autonomous driving. As revealed by cognitive neuroscientists, the amygdala of the brain can elicit defensive responses against threats or hazards, which is crucial for survival in and adaptation to risky environments. Drawing inspiration from this scientific discovery, we present a fear-neuro-inspired reinforcement learning framework to realize safe autonomous driving through modeling the amygdala functionality. This new technique facilitates an agent to learn defensive behaviors and achieve safe decision making with fewer safety violations. Through experimental tests, we show that the proposed approach enables the autonomous driving agent to attain state-of-the-art performance compared to the baseline agents and perform comparably to 30 certified human drivers, across various safety-critical scenarios. The results demonstrate the feasibility and effectiveness of our framework while also shedding light on the crucial role of simulating the amygdala function in the application of reinforcement learning to safety-critical autonomous driving domains. Xiangkun He, Jingda Wu, Zhiyu Huang, Zhongxu Hu, Jun Wang 0012, Alberto L. Sangiovanni-Vincentelli, Chen Lv 0001 |
IEEE Trans. Pattern Anal. Mach. Intell. | 6 |
| 2024 | Synthesizing LTL contracts from component libraries using rich counterexamplesabstractWe provide a method to synthesize an LTL Assume/Guarantee (A/G) specification, or contract, as an interconnection of elements from a library, each of which is also represented by an LTL A/G contract. Our approach, based on counterexample-guided inductive synthesis, leverages an off-the-shelf model checker to reason about infinite-length counterexamples and guarantee correctness. To increase scalability, we also introduce a novel concept of specification decomposition, based on contract projections; we show how it can be used to break down our synthesis problem into several simpler tasks, without reducing the size of the solution space. We test our technique on three industry-relevant case studies. Antonio Iannopollo, Inigo Incer, Alberto L. Sangiovanni-Vincentelli |
Sci. Comput. Program. | 3 |
| 2024 | Floorplet: Performance-Aware Floorplan Framework for Chiplet IntegrationabstractA chiplet is an integrated circuit (IC) that encompasses a well-defined subset of an overall systems functionality. In contrast to traditional monolithic system-on-chips (SoCs), chipletbased architecture can reduce costs and increase reusability, representing a promising avenue for continuing Moore’s Law. Despite the advantages of multi-chiplet architectures, floorplan design in a chiplet-based architecture has received limited attention. Conflicts between cost and performance necessitate a trade-off in chiplet floorplan design since additional latency introduced by advanced packaging can decrease performance. Consequently, balancing performance, cost, area, and reliability is of paramount importance. To address this challenge, we propose Floorplet (Floorplan chiplet), a framework comprising simulation tools for performance reporting and comprehensive models for cost and reliability optimization. Our framework employs the open-source Gem5 simulator to establish the relationship between performance and floorplan for the first time, guiding the floorplan optimization of multi-chiplet architecture. The experimental results show that our method decreases inter-chiplet communication costs by 24.81%. Shixin Chen, Shanyi Li, Zhen Zhuang, Su Zheng, Zheng Liang 0003, Tsung-Yi Ho, Bei Yu 0001, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 8 |
| 2024 | Efficient Encodings for Scalable Exploration of Cyber-Physical System ArchitecturesabstractWe present a methodology for scalable exploration of cyber-physical system architectures. We propose a mathematical formulation of the architecture exploration problem as an optimized mapping problem that includes joint selection of system topologies and components taken from predefined libraries. Using a graph-based representation of an architecture, we introduce novel compact encodings of mapping constraints and path constraints that significantly improve the scalability of the formulation. We use the new encodings to instantiate design requirements, such as interconnection, routing, timing, and energy constraints, on the architecture model. We implement our methods in an extensible architecture exploration toolbox, and provide a pattern-based language for formal, yet flexible, requirement specification. Numerical evaluations on a set of design problems from wireless sensor networks, reconfigurable manufacturing systems, and electrical power systems demonstrate the effectiveness of our approach. Dmitrii Kirov, Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Roberto Passerone |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2023 | 3D Environment Modeling for Falsification and Beyond with Scenic 3.0abstractAbstract We present a major new version of Scenic, a probabilistic programming language for writing formal models of the environments of cyber-physical systems. Scenic has been successfully used for the design and analysis of CPS in a variety of domains, but earlier versions are limited to environments that are essentially two-dimensional. In this paper, we extend Scenic with native support for 3D geometry, introducing new syntax that provides expressive ways to describe 3D configurations while preserving the simplicity and readability of the language. We replace Scenic’s simplistic representation of objects as boxes with precise modeling of complex shapes, including a ray tracing-based visibility system that accounts for object occlusion. We also extend the language to support arbitrary temporal requirements expressed in LTL, and build an extensible Scenic parser generated from a formal grammar of the language. Finally, we illustrate the new application domains these features enable with case studies that would have been impossible to accurately model in Scenic 2. Eric Vin, Shun Kashiwa, Matthew Rhea, Daniel J. Fremont, Edward Kim 0005, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue 0001, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
CAV (1) | 9 |
| 2023 | Beating Backdoor Attack at Its Own GameabstractDeep neural networks (DNNs) are vulnerable to backdoor attack, which does not affect the network’s performance on clean data but would manipulate the network behavior once a trigger pattern is added. Existing defense methods have greatly reduced attack success rate, but their prediction accuracy on clean data still lags behind a clean model by a large margin. Inspired by the stealthiness and effectiveness of backdoor attack, we propose a simple but highly effective defense framework which injects non-adversarial backdoors targeting poisoned samples. Following the general steps in backdoor attack, we detect a small set of suspected samples and then apply a poisoning strategy to them. The non-adversarial backdoor, once triggered, suppresses the attacker’s backdoor on poisoned data, but has limited influence on clean data. The defense can be carried out during data preprocessing, without any modification to the standard end-to-end training pipeline. We conduct extensive experiments on multiple benchmarks with different architectures and representative attacks. Results demonstrate that our method achieves state-of-the-art defense effectiveness with by far the lowest performance drop on clean data. Considering the surprising defense ability displayed by our framework, we call for more attention to utilizing backdoor for backdoor defense. Code is available at https://github.com/damianliumin/non-adversarial_backdoor. Alberto L. Sangiovanni-Vincentelli, Xiangyu Yue 0001 |
ICCV | 2 |
| 2023 | Automated Design of ChipletsabstractChiplet-based designs have gained recognition as a promising alternative to monolithic SoCs due to their lower manufacturing costs, improved re-usability, and optimized technology specialization. Despite progress made in various related domains, the design of chiplets remains largely reliant on manual processes. In this paper, we provide an examination of the historical evolution of chiplets, encompassing a review of crucial design considerations and a synopsis of recent advancements in relevant fields. Further, we identify and examine the opportunities and challenges in the automated design of chiplets. To further demonstrate the potential of this nascent area, we present a novel task that Alberto L. Sangiovanni-Vincentelli, Zheng Liang 0003, Zhe Zhou 0002, Jiaxi Zhang 0001 |
ISPD | 1 |
| 2023 | Contract Replaceability for Ensuring Independent Design using Assume-Guarantee Contracts
Sheng-Jung Yu, Inigo Incer, Alberto L. Sangiovanni-Vincentelli |
MEMOCODE | 3 |
| 2023 | Constraint-Behavior Contracts: A Formalism for Specifying Physical Systems
Sheng-Jung Yu, Inigo Incer, Alberto L. Sangiovanni-Vincentelli |
MEMOCODE | 3 |
| 2023 | Scenic: a language for scenario specification and data generationabstractAbstract We propose a new probabilistic programming language for the design and analysis of cyber-physical systems, especially those based on machine learning. We consider several problems arising in the design process, including training a system to be robust to rare events, testing its performance under different conditions, and debugging failures. We show how a probabilistic programming language can help address these problems by specifying distributions encoding interesting types of inputs, then sampling these to generate specialized training and test data. More generally, such languages can be used to write environment models, an essential prerequisite to any formal analysis. In this paper, we focus on systems such as autonomous cars and robots, whose environment at any point in time is a scene , a configuration of physical objects and agents. We design a domain-specific language, Scenic , for describing scenarios that are distributions over scenes and the behaviors of their agents over time. Scenic combines concise, readable syntax for spatiotemporal relationships with the ability to declaratively impose hard and soft constraints over the scenario. We develop specialized techniques for sampling from the resulting distribution, taking advantage of the structure provided by Scenic ’s domain-specific syntax. Finally, we apply Scenic in multiple case studies for training, testing, and debugging neural networks for perception both as standalone components and within the context of a full cyber-physical system. Daniel J. Fremont, Edward Kim 0005, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue 0001, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
Mach. Learn. | 6 |
| 2022 | Programmatic Modeling and Generation of Real-Time Strategic Soccer Environments for Reinforcement LearningabstractThe capability of a reinforcement learning (RL) agent heavily depends on the diversity of the learning scenarios generated by the environment. Generation of diverse realistic scenarios is challenging for real-time strategy (RTS) environments. The RTS environments are characterized by intelligent entities/non-RL agents cooperating and competing with the RL agents with large state and action spaces over a long period of time, resulting in an infinite space of feasible, but not necessarily realistic, scenarios involving complex interaction among different RL and non-RL agents. Yet, most of the existing simulators rely on randomly generating the environments based on predefined settings/layouts and offer limited flexibility and control over the environment dynamics for researchers to generate diverse, realistic scenarios as per their demand. To address this issue, for the first time, we formally introduce the benefits of adopting an existing formal scenario specification language, SCENIC, to assist researchers to model and generate diverse scenarios in an RTS environment in a flexible, systematic, and programmatic manner. To showcase the benefits, we interfaced SCENIC to an existing RTS environment Google Research Football (GRF) simulator and introduced a benchmark consisting of 32 realistic scenarios, encoded in SCENIC, to train RL agents and testing their generalization capabilities. We also show how researchers/RL practitioners can incorporate their domain knowledge to expedite the training process by intuitively modeling stochastic programmatic policies with SCENIC. Abdus Salam Azad, Edward Kim 0005, Qiancheng Wu, Kimin Lee, Ion Stoica, Pieter Abbeel, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
AAAI | 7 |
| 2022 | Conditional Synthetic Data Generation for Robust Machine Learning Applications with Limited Pandemic DataabstractBackground: At the onset of a pandemic, such as COVID-19, data with proper labeling/attributes corresponding to the new disease might be unavailable or sparse. Machine Learning (ML) models trained with the available data, which is limited in quantity and poor in diversity, will often be biased and inaccurate. At the same time, ML algorithms designed to fight pandemics must have good performance and be developed in a time-sensitive manner. To tackle the challenges of limited data, and label scarcity in the available data, we propose generating conditional synthetic data, to be used alongside real data for developing robust ML models. Methods: We present a hybrid model consisting of a conditional generative flow and a classifier for conditional synthetic data generation. The classifier decouples the feature representation for the condition, which is fed to the flow to extract the local noise. We generate synthetic data by manipulating the local noise with fixed conditional feature representation. We also propose a semi-supervised approach to generate synthetic samples in the absence of labels for a majority of the available data. Results: We performed conditional synthetic generation for chest computed tomography (CT) scans corresponding to normal, COVID-19, and pneumonia afflicted patients. We show that our method significantly outperforms existing models both on qualitative and quantitative performance, and our semi-supervised approach can efficiently synthesize conditional samples under label scarcity. As an example of downstream use of synthetic data, we show improvement in COVID-19 detection from CT scans with conditional synthetic data augmentation. Hari Prasanna Das, Ryan Tran, Japjot Singh, Xiangyu Yue 0001, Geoffrey H. Tison, Alberto L. Sangiovanni-Vincentelli, Costas J. Spanos |
AAAI | 6 |
| 2022 | Emotional Semantics-Preserved and Feature-Aligned CycleGAN for Visual Emotion AdaptationabstractThanks to large-scale labeled training data, deep neural networks (DNNs) have obtained remarkable success in many vision and multimedia tasks. However, because of the presence of domain shift, the learned knowledge of the well-trained DNNs cannot be well generalized to new domains or datasets that have few labels. Unsupervised domain adaptation (UDA) studies the problem of transferring models trained on one labeled source domain to another unlabeled target domain. In this article, we focus on UDA in visual emotion analysis for both emotion distribution learning and dominant emotion classification. Specifically, we design a novel end-to-end cycle-consistent adversarial model, called CycleEmotionGAN++. First, we generate an adapted domain to align the source and target domains on the pixel level by improving CycleGAN with a multiscale structured cycle-consistency loss. During the image translation, we propose a dynamic emotional semantic consistency loss to preserve the emotion labels of the source images. Second, we train a transferable task classifier on the adapted domain with feature-level alignment between the adapted and target domains. We conduct extensive UDA experiments on the Flickr-LDL and Twitter-LDL datasets for distribution learning and ArtPhoto and Flickr and Instagram datasets for emotion classification. The results demonstrate the significant improvements yielded by the proposed CycleEmotionGAN++ compared to state-of-the-art UDA approaches. Sicheng Zhao, Xuanbai Chen, Xiangyu Yue 0001, Chuang Lin 0003, Pengfei Xu 0013, Ravi Krishna, Jufeng Yang, Guiguang Ding, Alberto L. Sangiovanni-Vincentelli, Kurt Keutzer |
IEEE Trans. Cybern. | 9 |
| 2022 | A Review of Single-Source Deep Unsupervised Visual Domain AdaptationabstractLarge-scale labeled training datasets have enabled deep neural networks to excel across a wide range of benchmark vision tasks. However, in many applications, it is prohibitively expensive and time-consuming to obtain large quantities of labeled data. To cope with limited labeled training data, many have attempted to directly apply models trained on a large-scale labeled source domain to another sparsely labeled or unlabeled target domain. Unfortunately, direct transfer across domains often performs poorly due to the presence of domain shift or dataset bias. Domain adaptation (DA) is a machine learning paradigm that aims to learn a model from a source domain that can perform well on a different (but related) target domain. In this article, we review the latest single-source deep unsupervised DA methods focused on visual tasks and discuss new perspectives for future research. We begin with the definitions of different DA strategies and the descriptions of existing benchmark datasets. We then summarize and compare different categories of single-source unsupervised DA methods, including discrepancy-based methods, adversarial discriminative methods, adversarial generative methods, and self-supervision-based methods. Finally, we discuss future research directions with challenges and possible solutions. Sicheng Zhao, Xiangyu Yue 0001, Shanghang Zhang, Bo Li 0080, Han Zhao 0002, Bichen Wu, Ravi Krishna, Joseph Gonzalez 0001, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Kurt Keutzer |
IEEE Trans. Neural Networks Learn. Syst. | 9 |
| 2021 | Prototypical Cross-Domain Self-Supervised Learning for Few-Shot Unsupervised Domain AdaptationabstractUnsupervised Domain Adaptation (UDA) transfers predictive models from a fully-labeled source domain to an unlabeled target domain. In some applications, however, it is expensive even to collect labels in the source domain, making most previous works impractical. To cope with this problem, recent work performed instance-wise cross-domain self-supervised learning, followed by an additional fine-tuning stage. However, the instance-wise self-supervised learning only learns and aligns low-level discriminative features. In this paper, we propose an end-to-end Prototypical Cross-domain Self-Supervised Learning (PCS) framework for Few-shot Unsupervised Domain Adaptation (FUDA)1. PCS not only performs cross-domain low-level feature alignment, but it also encodes and aligns semantic structures in the shared embedding space across domains. Our framework captures category-wise semantic structures of the data by in-domain prototypical contrastive learning; and performs feature alignment through cross-domain prototypical self-supervision. Compared with state-of-the-art methods, PCS improves the mean classification accuracy over different domain pairs on FUDA by 10.5%, 3.5%, 9.0%, and 13.2% on Office, Office-Home, VisDA-2017, and DomainNet, respectively. Xiangyu Yue 0001, Zangwei Zheng, Shanghang Zhang, Yang Gao 0029, Trevor Darrell, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli |
CVPR | 7 |
| 2021 | Safety in Autonomous Driving: Can Tools Offer Guarantees?abstractPersistent challenges in making autonomous vehicles safe and reliable have hampered their widespread deployment. We believe that formal methods will play an essential role in the enterprise of ensuring AV safety by providing tools for the modeling, verification, synthesis, and runtime assurance of AV systems. In this paper, we outline the progress we and others have made towards this goal, and the challenges that remain. Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
DAC | 2 |
| 2021 | The cyber-physical immune system: work-in-progressabstractCyber-Physical Systems (CPS) are important components of critical infrastructure and must operate with high levels of reliability and security. We propose a conceptual approach to securing CPSs: the Cyber-Physical Immune System (CPIS), a collection of hardware and software elements deployed on top of a conventional CPS. Inspired by its biological counterpart, the CPIS comprises an independent network of distributed computing units that collects data from the conventional CPS, utilizes data-driven techniques to identify threats, adapts to the changing environment, alerts the user of any threats or anomalies, and deploys threat-mitigation strategies. Ashank Verma, Jingchao Zhou, Inigo Incer, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 5 |
| 2021 | Scene-aware Learning Network for Radar Object DetectionabstractObject detection is essential to safe autonomous or assisted driving. Previous works usually utilize RGB images or LiDAR point clouds to identify and localize multiple objects in self-driving. However, cameras tend to fail in bad driving conditions, e.g. bad weather or weak lighting, while LiDAR scanners are too expensive to get widely deployed in commercial applications. Radar has been drawing more and more attention due to its robustness and low cost. In this paper, we propose a scene-aware radar learning framework for accurate and robust object detection. First, the learning framework contains branches conditioning on the scene category of the radar sequence; with each branch optimized for a specific type of scene. Second, three different 3D autoencoder-based architectures are proposed for radar object detection and ensemble learning is performed over the different architectures to further boost the final performance. Third, we propose novel scene-aware sequence mix augmentation (SceneMix) and scene-specific post-processing to generate more robust detection results. In the ROD2021 Challenge, we achieved a final result of average precision of 75.0% and an average recall of 81.0%. Moreover, in the parking lot scene, our framework ranks first with an average precision of 97.8% and an average recall of 98.6%, which demonstrates the effectiveness of our framework. Zangwei Zheng, Xiangyu Yue 0001, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli |
ICMR | 4 |
| 2021 | AVDM: A hierarchical command-and-control system architecture for cooperative autonomous vehicles in highways scenario using microscopic simulations
Thomas Braud, Jordan Ivanchev, Corvin Deboeser, Alois C. Knoll, David Eckhoff, Alberto L. Sangiovanni-Vincentelli |
Auton. Agents Multi Agent Syst. | 6 |
| 2021 | Adaptive Body Area Networks Using Kinematics and BiosignalsabstractThe increasing penetration of wearable and implantable devices necessitates energy-efficient and robust ways of connecting them to each other and to the cloud. However, the wireless channel around the human body poses unique challenges such as a high and variable path-loss caused by frequent changes in the relative node positions as well as the surrounding environment. An adaptive wireless body area network (WBAN) scheme is presented that reconfigures the network by learning from body kinematics and biosignals. It has very low overhead since these signals are already captured by the WBAN sensor nodes to support their basic functionality. Periodic channel fluctuations in activities like walking can be exploited by reusing accelerometer data and scheduling packet transmissions at optimal times. Network states can be predicted based on changes in observed biosignals to reconfigure the network parameters in real time. A realistic body channel emulator that evaluates the path-loss for everyday human activities was developed to assess the efficacy of the proposed techniques. Simulation results show up to 41% improvement in packet delivery ratio (PDR) and up to 27% reduction in power consumption by intelligent scheduling at lower transmission power levels. Moreover, experimental results on a custom test-bed demonstrate an average PDR increase of 20% and 18% when using our adaptive EMG- and heart-rate-based transmission power control methods, respectively. The channel emulator and simulation code is made publicly available at https://github.com/a-moin/wban-pathloss. Ali Moin, Arno Thielens, Álvaro Araujo, Alberto L. Sangiovanni-Vincentelli, Jan M. Rabaey |
IEEE J. Biomed. Health Informatics | 4 |
| 2020 | ODRE Workshop: Probabilistic Dynamic Hard Real-Time Scheduling in HPCabstractIndustry 4.0 is changing fundamentally the way data is collected, stored and analyzed in industrial processes. While this change enables novel application such as flexible manufacturing of highly customized products, the real-time control of these processes, however, has not yet realized its full potential. We believe that modern virtualization techniques, specifically application containers, present a unique opportunity to decouple control functionality from associated hardware. Through it, we can fully realize the potential for highly distributed and transferable industrial processes even with real-time constraints arising from time-critical sub-processes. In this paper, we present a specifically developed orchestration tool to manage the challenges and opportunities of shifting industrial control software from dedicated hardware to bare-metal servers or (edge) cloud computing platforms. Using off-the-shelf technology, the proposed tool can manage the execution of containerized applications on shared resources without compromising hard real-time execution determinism. Through first experimental results, we confirm the viability and analyzed the behavior of resource shared systems with strict real-time requirements. We then describe experiments set out to deliver expected results and gather performance, application scope and limits of the presented approach. Florian Hofer 0001, Martin A. Sehr, Barbara Russo, Alberto L. Sangiovanni-Vincentelli |
ISORC | 4 |
| 2020 | Optimized Selection of Reliable and Cost-Effective Safety-Critical System ArchitecturesabstractWe address the problem of synthesizing safety-critical embedded and cyber-physical system architectures to minimize a cost function while guaranteeing the desired reliability. We represent a system architecture as a configurable graph in which both the nodes (components) and edges (interconnections) may fail. We then propose a compact analytical formalism to efficiently reason about the reliability of the overall system based on the failure probabilities of the components, and provide expressions of the design constraints that avoid exhaustive enumeration of failure cases on all possible graph configurations. Based on these constraints, we cast the synthesis problem as an optimization problem and propose monolithic and iterative optimization schemes to decrease the problem complexity. We implement the proposed algorithms in the ArchEx framework, leveraging a pattern-based specification language to facilitate problem formulation. Design problems from aircraft electric power distribution networks and reconfigurable industrial manufacturing systems illustrate the effectiveness of our approach. Pierluigi Nuzzo 0002, Nikunj Bajaj, Michael Masin, Dmitrii Kirov, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 6 |
| 2020 | Gordian: Formal Reasoning-based Outlier Detection for Secure LocalizationabstractAccurate localization from Cyber-Physical Systems (CPS) is a critical enabling technology for context-aware applications and control. As localization plays an increasingly safety-critical role, location systems must be able to identify and eliminate faulty measurements to prevent dangerously inaccurate localization. In this article, we consider the range-based localization problem and propose a method to detect coordinated adversarial corruption on anchor positions and distance measurements. Our algorithm, G ordian , rapidly finds attacks by identifying geometric inconsistencies at the graph level without requiring assumptions about hardware, ranging mechanisms, or cryptographic protocols. We give necessary conditions for which attack detection is guaranteed to be successful in the noiseless case, and we use that intuition to extend G ordian to the noisy case where fewer guarantees are possible. In simulations generated from real-world sensor noise, we empirically show that G ordian ’s trilateration counterexample generation procedure enables rapid attack detection even for combinatorially difficult problems. Matthew Weber, Baihong Jin, Gil Lederman, Yasser Shoukry, Edward A. Lee, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Cyber Phys. Syst. | 7 |
| 2019 | Beyond Schematic Capture: Meaningful Abstractions for Better Electronics Design ToolsabstractPrinted Circuit Board (PCB) design tools are critical in helping users build non-trivial electronics devices. While recent work recognizes deficiencies with current tools and explores novel methods, little has been done to understand modern designers and their needs. To gain better insight into their practices, we interview fifteen electronics designers of a variety of backgrounds. Our open-ended, semi-structured interviews examine both overarching design flows and details of individual steps. One major finding was that most creative engineering work happens during system architecture, yet current tools operate at lower abstraction levels and create significant tedious work for designers. From that insight, we conceptualize abstractions and primitives for higher-level tools and elicit feedback from our participants on clickthrough mockups of design flows through an example project. We close with our observation on opportunities for improving board design tools and discuss generalizability of our findings beyond the electronics domain. Richard Lin, Rohit Ramesh, Antonio Iannopollo, Alberto L. Sangiovanni-Vincentelli, Prabal Dutta, Elad Alon, Björn Hartmann |
CHI | 4 |
| 2019 | Industrial Control via Application Containers: Migrating from Bare-Metal to IAASabstractWe explore the challenges and opportunities of shifting industrial control software from dedicated hardware to bare-metal servers or cloud computing platforms using off the shelf technologies. In particular, we demonstrate that executing time-critical applications on cloud platforms is viable based on a series of dedicated latency tests targeting relevant real-time configurations. Florian Hofer 0001, Martin A. Sehr, Antonio Iannopollo, Ines Ugalde, Alberto L. Sangiovanni-Vincentelli, Barbara Russo |
CloudCom | 5 |
| 2019 | A new simulation metric to determine safe environments and controllers for systems with unknown dynamicsabstractWe consider the problem of extracting safe environments and controllers for reach-avoid objectives for systems with known state and control spaces, but unknown dynamics. In a given environment, a common approach is to synthesize a controller from an abstraction or a model of the system (potentially learned from data). However, in many situations, the relationship between the dynamics of the model and the actual system is not known; and hence it is difficult to provide safety guarantees for the system. In such cases, the Standard Simulation Metric (SSM), defined as the worst-case norm distance between the model and the system output trajectories, can be used to modify a reach-avoid specification for the system into a more stringent specification for the abstraction. Nevertheless, the obtained distance, and hence the modified specification, can be quite conservative. This limits the set of environments for which a safe controller can be obtained. We propose SPEC, a specification-centric simulation metric, which overcomes these limitations by computing the distance using only the trajectories that violate the specification for the system. We show that modifying a reach-avoid specification with SPEC allows us to synthesize a safe controller for a larger set of environments compared to SSM. We also propose a probabilistic method to compute SPEC for a general class of systems. Case studies using simulators for quadrotors and autonomous cars illustrate the advantages of the proposed metric for determining safe environment sets and controllers. Shromona Ghosh, Somil Bansal, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Claire J. Tomlin |
HSCC | 3 |
| 2019 | Domain Randomization and Pyramid Consistency: Simulation-to-Real Generalization Without Accessing Target Domain DataabstractWe propose to harness the potential of simulation for semantic segmentation of real-world self-driving scenes in a domain generalization fashion. The segmentation network is trained without any information about target domains and tested on the unseen target domains. To this end, we propose a new approach of domain randomization and pyramid consistency to learn a model with high generalizability. First, we propose to randomize the synthetic images with styles of real images in terms of visual appearances using auxiliary datasets, in order to effectively learn domain-invariant representations. Second, we further enforce pyramid consistency across different "stylized" images and within an image, in order to learn domain-invariant and scale-invariant features, respectively. Extensive experiments are conducted on generalization from GTA and SYNTHIA to Cityscapes, BDDS, and Mapillary; and our method achieves superior results over the state-of-the-art techniques. Remarkably, our generalization results are on par with or even better than those obtained by state-of-the-art simulation-to-real domain adaptation methods, which access the target domain data at training time. Xiangyu Yue 0001, Yang Zhang 0035, Sicheng Zhao, Alberto L. Sangiovanni-Vincentelli, Kurt Keutzer, Boqing Gong |
ICCV | 4 |
| 2019 | An Encoder-Decoder Based Approach for Anomaly Detection with Application in Additive ManufacturingabstractWe present a novel unsupervised deep learning approach that utilizes an encoder-decoder architecture for detecting anomalies in sequential sensor data collected during industrial manufacturing. Our approach is designed to not only detect whether there exists an anomaly at a given time step, but also to predict what will happen next in the (sequential) process. We demonstrate our approach on a dataset collected from a real-world Additive Manufacturing (AM) testbed. The dataset contains infrared (IR) images collected under both normal conditions and synthetic anomalies. We show that our encoder-decoder model is able to identify the injected anomalies in a modern AM manufacturing process in an unsupervised fashion. In addition, our approach also gives hints about the temperature non-uniformity of the testbed during manufacturing, which was not previously known prior to the experiment. Yingshui Tan, Baihong Jin, Alexander J. Nettekoven, Yuxin Chen 0001, Yisong Yue, Ufuk Topcu, Alberto L. Sangiovanni-Vincentelli |
ICMLA | 7 |
| 2019 | My 50-Year Journey from Punched Cards to Swarm SystemsabstractThe article is a reflection onmy journey during the development of the EDA field, from its early days to its explosive growth and present maturity. The two special issues of the Solid State Circuit Society Magazine "Corsi e Ricorsi: Alberto Sangiovanni Vincentelli and the Evolution of EDA", published in 2010 [1,2], contain a set of papers that pinpoint some of the stages of this journey. Alberto L. Sangiovanni-Vincentelli |
ISPD | 1 |
| 2019 | Scenic: a language for scenario specification and scene generationabstractWe propose a new probabilistic programming language for the design and analysis of perception systems, especially those based on machine learning. Specifically, we consider the problems of training a perception system to handle rare events, testing its performance under different conditions, and debugging failures. We show how a probabilistic programming language can help address these problems by specifying distributions encoding interesting types of inputs and sampling these to generate specialized training and test sets. More generally, such languages can be used for cyber-physical systems and robotics to write environment models, an essential prerequisite to any formal analysis. In this paper, we focus on systems like autonomous cars and robots, whose environment is a scene, a configuration of physical objects and agents. We design a domain-specific language, Scenic, for describing scenarios that are distributions over scenes. As a probabilistic programming language, Scenic allows assigning distributions to features of the scene, as well as declaratively imposing hard and soft constraints over the scene. We develop specialized techniques for sampling from the resulting distribution, taking advantage of the structure provided by Scenic's domain-specific syntax. Finally, we apply Scenic in a case study on a convolutional neural network designed to detect cars in road images, improving its performance beyond that achieved by state-of-the-art synthetic data generation methods. Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue 0001, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
PLDI | 5 |
| 2019 | Constrained synthesis from component libraries
Antonio Iannopollo, Stavros Tripakis, Alberto L. Sangiovanni-Vincentelli |
Sci. Comput. Program. | 3 |
| 2019 | Stochastic Assume-Guarantee Contracts for Cyber-Physical System DesignabstractWe present an assume-guarantee contract framework for cyber-physical system design under probabilistic requirements. Given a stochastic linear system and a set of requirements captured by bounded Stochastic Signal Temporal Logic (StSTL) contracts, we propose algorithms to check contract compatibility, consistency, and refinement, and generate a sequence of control inputs that satisfies a contract. We leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce sound and tractable problem formulations. We illustrate the effectiveness of our approach on three case studies, including the design of controllers for aircraft power distribution networks. Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Yugeng Xi 0001, Dewei Li 0001 |
ACM Trans. Embed. Comput. Syst. | 3 |
| 2019 | Coherent Extension, Composition, and Merging Operators in Contract Models for System DesignabstractContract models have been proposed to promote and facilitate reuse and distributed development. In this paper, we cast contract models into a coherent formalism used to derive general results about the properties of their operators. We study several extensions of the basic model, including the distinction between weak and strong assumptions and maximality of the specification. We then analyze the disjunction and conjunction operators, and show how they can be broken up into a sequence of simpler operations. This leads to the definition of a new contract viewpoint merging operator, which better captures the design intent in contrast to the more traditional conjunction. The adjoint operation, which we call separation, can be used to re-partition the specification into different viewpoints. We show the symmetries of these operations with respect to composition and quotient. Roberto Passerone, Inigo Incer, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Embed. Comput. Syst. | 3 |
| 2018 | Optimized selection of wireless network topologies and components via efficient pruning of feasible pathsabstractWe address the design space exploration of wireless networks to jointly select topology and component sizing. We formulate the exploration problem as an optimized mapping problem, where network elements are associated with components from pre-defined libraries to minimize a cost function under correctness guarantees. We express a rich set of system requirements as mixed integer linear constraints over path variables, denoting the presence or absence of paths between network nodes, and propose an algorithm for efficient, compact encoding of feasible paths that can reduce by orders of magnitude the complexity of the optimization problem. We incorporate our methods in a system-level design space exploration toolbox and evaluate their effectiveness on design examples from data collection and localization networks. Dmitrii Kirov, Pierluigi Nuzzo 0002, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 2018 | Specification decomposition for synthesis from libraries of LTL Assume/Guarantee contractsabstractContract-Based Design is a methodology that allows for compositional design of complex systems. Given a contract representing a specification, it is possible to formally satisfy it by composing a number of simpler contracts. When these simpler contracts are chosen from a library of existing solutions, we talk about synthesis from contract libraries. There are techniques to automate the synthesis process, but they are computationally intensive, especially for complex specifications. In this paper, we describe an efficient technique to partition a specification, i.e., an LTL-based Assume/Guarantee contract, in a number of simpler sub-specifications which can be satisfied independently. Once all these smaller problems are solved, it is possible to safely merge their solutions to satisfy the original specification. We show the effectiveness of our technique in an industrial case study. Antonio Iannopollo, Stavros Tripakis, Alberto L. Sangiovanni-Vincentelli |
DATE | 3 |
| 2018 | CHASE: Contract-based requirement engineering for cyber-physical system designabstractThis paper presents CHASE, a framework for requirement capture, formalization, and validation for cyber-physical systems. CHASE combines a practical front-end formal specification language based on patterns with a rigorous verification back-end based on assume-guarantee contracts. The front-end language can express temporal properties of networks using a declarative style, and supports automatic translation from natural-language constructs to low-level mathematical languages. The verification back-end leverages the mathematical formalism of contracts to reason about system requirements and determine inconsistencies and dependencies between them. CHASE features a modular and extensible software infrastructure that can support different domain-specific languages, modeling formalisms, and analysis tools. We illustrate its effectiveness on industrial design examples, including control of aircraft power distribution networks and arbitration of a mixed-criticality automotive bus. Pierluigi Nuzzo 0002, Michele Lora, Yishai A. Feldman, Alberto L. Sangiovanni-Vincentelli |
DATE | 4 |
| 2018 | Counterexample-Guided Data AugmentationabstractWe present a novel framework for augmenting data sets for machine learning based on counterexamples. Counterexamples are misclassified examples that have important properties for retraining and improving the model. Key components of our framework include a \textit{counterexample generator}, which produces data items that are misclassified by the model and error tables, a novel data structure that stores information pertaining to misclassifications. Error tables can be used to explain the model's vulnerabilities and are used to efficiently generate counterexamples for augmentation. We show the efficacy of the proposed framework by comparing it to classical augmentation techniques on a case study of object detection in autonomous driving based on deep neural networks. Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue 0001, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
IJCAI | 5 |
| 2018 | Quotient for Assume-Guarantee ContractsabstractWe introduce a novel notion of quotient set for a pair of contracts and the operation of quotient for assume-guarantee contracts. The quotient set and its related operation can be used in any compositional methodology where design requirements are mapped into a set of components in a library. In particular, they can be used for the so called missing component problem, where the given components are not capable of discharging the obligations of the requirements. In this case, the quotient operation identifies the contract for a component that, if added to the original set, makes the resulting system fulfill the requirements. Inigo Incer, Alberto L. Sangiovanni-Vincentelli, Chung-Wei Lin, Eunsuk Kang |
MEMOCODE | 2 |
| 2018 | A LiDAR Point Cloud Generator: from a Virtual World to Autonomous Drivingabstract3D LiDAR scanners are playing an increasingly important role in autonomous driving as they can generate depth information of the environment. However, creating large 3D LiDAR point cloud datasets with point-level labels requires a significant amount of manual annotation. This jeopardizes the efficient development of supervised deep learning algorithms which are often data-hungry. We present a framework to rapidly create point clouds with accurate point-level labels from a computer game. To our best knowledge, this is the first publication on LiDAR point cloud simulation framework for autonomous driving. The framework supports data collection from both auto-driving scenes and user-configured scenes. Point clouds from auto-driving scenes can be used as training data for deep learning algorithms, while point clouds from user-configured scenes can be used to systematically test the vulnerability of a neural network, and use the falsifying examples to make the neural network more robust through retraining. In addition, the scene images can be captured simultaneously in order for sensor fusion tasks, with a method proposed to do automatic registration between the point clouds and captured scene images. We show a significant improvement in accuracy (+9%) in point cloud segmentation by augmenting the training dataset with the generated synthesized data. Our experiments also show by testing and retraining the network using point clouds from user-configured scenes, the weakness/blind spots of the neural network can be fixed. Xiangyu Yue 0001, Bichen Wu, Sanjit A. Seshia, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli |
ICMR | 5 |
| 2018 | Time-Series Learning Using Monotonic Logical Properties
Marcell Vazquez-Chanlatte, Shromona Ghosh, Jyotirmoy V. Deshmukh, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
RV | 4 |
| 2018 | Design Automation for Smart Building SystemsabstractSmart buildings today are aimed at providing safe, healthy, comfortable, affordable, and beautiful spaces in a carbon and energy-efficient way. They are emerging as complex cyber-physical systems with humans in the loop. Cost, the need to cope with increasing functional complexity, flexibility, fragmentation of the supply chain, and time-to-market pressure are rendering the traditional heuristic and ad hoc design paradigms inefficient and insufficient for the future. In this paper, we present a platform-based methodology for smart building design. Platform-based design (PBD) promotes the reuse of hardware and software on shared infrastructures, enables rapid prototyping of applications, and involves extensive exploration of the design space to optimize design performance. In this paper, we identify, abstract, and formalize components of smart buildings, and present a design flow that maps high-level specifications of desired building applications to their physical implementations under the PBD framework. A case study on the design of on-demand heating, ventilation, and air conditioning (HVAC) systems is presented to demonstrate the use of PBD. Ruoxi Jia 0001, Baihong Jin, Ming Jin 0002, Yuxun Zhou, Ioannis C. Konstantakopoulos, Han Zou, Joyce Kim, Dan Li 0016, Weixi Gu, Reza Arghandeh, Pierluigi Nuzzo 0002, Stefano Schiavon, Alberto L. Sangiovanni-Vincentelli, Costas J. Spanos |
Proc. IEEE | 13 |
| 2018 | SMC: Satisfiability Modulo Convex ProgrammingabstractThe design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of “cyber” components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming. Yasser Shoukry, Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, Paulo Tabuada |
Proc. IEEE | 3 |
| 2018 | Codesign Methodologies and Tools for Cyber-Physical SystemsabstractCyber-physical system (CPS) analysis and design are challenging due to the intrinsic heterogeneity of those systems. Today, CPSs are often designed by leveraging existing solutions and by adding cyber components to an existing physical system, thus decomposing the design into two separate phases. In this paper, we argue that the codesign of the cyber and physical components would expose solutions that are better under all aspects, such as safety, efficiency, security, performance, reliability, fault tolerance, and extensibility. To do so, automated codesign tools are a necessity due to the complexity of the problems at hand. In the paper, we will discuss the key needs and challenges in developing modeling, simulation, synthesis, validation, and verification tools for CPS codesign, present promising codesign approaches from our teams and others, and point out where additional research is needed. Qi Zhu 0002, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 2 |
| 2018 | Design Automation for Cyber-Physical Systems [Scanning the Issue]abstractCyber-physical systems (CPSs) are characterized by the seamless integration and close interaction of cyber components (e.g., sensors, computation nodes, communication networks) and physical processes (e.g., mechanical devices, physical environment, humans). The cyber components monitor, analyze, and control the physical processes, and react to their changes through feedback loops. A classic example of CPSs is autonomous vehicles. These vehicles collect information of the surrounding physical environment via heterogeneous sensors such as cameras, radar, and LIDAR; process and analyze the multi-modal information at real time with advanced computing devices such as GPUs, application-specific SoCs and multicore CPUs; automatically make planning and control decisions; and continuously actuate the corresponding mechanical components. The cyber components of autonomous vehicles are much more intelligent and complex than those of traditional vehicles, and interact more directly and closely with the physical environment. Qi Zhu 0002, Alberto L. Sangiovanni-Vincentelli, Shiyan Hu 0001, Xin Li 0001 |
Proc. IEEE | 2 |
| 2018 | A Model-based approach for the synthesis of software to firmware adapters for use with automatically generated components
Marco Di Natale, David Perillo, Francesco Chirico, Andrea Sindico, Alberto L. Sangiovanni-Vincentelli |
Softw. Syst. Model. | 5 |
| 2018 | SMT-Based Observer Design for Cyber-Physical Systems under Sensor AttacksabstractWe introduce a scalable observer architecture, which can efficiently estimate the states of a discrete-time linear-time-invariant system whose sensors are manipulated by an attacker, and is robust to measurement noise. Given an upper bound on the number of attacked sensors, we build on previous results on necessary and sufficient conditions for state estimation, and propose a novel Multi-Modal Luenberger (MML) observer based on efficient Satisfiability Modulo Theory (SMT) solving. We present two techniques to reduce the complexity of the estimation problem. As a first strategy, instead of a bank of distinct observers, we use a family of filters sharing a single dynamical equation for the states, but different output equations, to generate estimates corresponding to different subsets of sensors. Such an architecture can reduce the memory usage of the observer from an exponential to a linear function of the number of sensors. We then develop an efficient SMT-based decision procedure that is able to reason about the estimates of the MML observer to detect at runtime which sets of sensors are attack-free, and use them to obtain a correct state estimate. Finally, we discuss two optimization-based algorithms that can efficiently select the observer parameters with the goal of minimizing the sensitivity of the estimates with respect to sensor noise. We provide proofs of convergence for our estimation algorithm and report simulation results to compare its runtime performance with alternative techniques. We show that our algorithm scales well for large systems (including up to 5,000 sensors) for which many previously proposed algorithms are not implementable due to excessive memory and time requirements. Finally, we illustrate the effectiveness of our approach, both in terms of resiliency to attacks and robustness to noise, on the design of large-scale power distribution networks. Yasser Shoukry, Michelle Chong, Masashi Wakaiki, Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, João Pedro Hespanha, Paulo Tabuada |
ACM Trans. Cyber Phys. Syst. | 5 |
| 2018 | A Mobile Health System for Neurocognitive Impairment Evaluation Based on P300 DetectionabstractA new mobile healthcare system for neuro-cognitive function monitoring and treatment is presented. The architecture of the system features sensors to measure the brain potential, localized data analysis and filtering, and in-cloud distribution to specialized medical personnel. As such, it presents tradeoffs typical of other cyber-physical systems, where hardware, algorithms, and software implementations have to come together in a coherent fashion. The system is based on spatio-temporal detection and characterization of a specific brain potential called P300. The diagnosis of cognitive deficit is achieved by analyzing the data collected by the system with a new algorithm called tuned-Residue Iteration Decomposition (t-RIDE). The system has been tested on 17 subjects ( n = 12 healthy, n = 3 mildly cognitive impaired, and n = 2 with Alzheimer's disease involved in three different cognitive tasks with increasing difficulty. The system allows fast diagnosis of cognitive deficit, including mild and heavy cognitive impairment: t-RIDE convergence is achieved in 79 iterations (i.e., 1.95s), yielding an 80% accuracy in P300 amplitude evaluation with only 13 trials on a single EEG channel. Daniela De Venuto, Valerio F. Annese, Giovanni Mezzina, Floriano Scioscia, Michele Ruta, Eugenio Di Sciascio, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Cyber Phys. Syst. | 7 |
| 2017 | ArchEx: An Extensible Framework for the Exploration of Cyber-Physical System ArchitecturesabstractWe present ArchEx, a framework for cyber-physical system architecture exploration. We formulate the exploration problem as a mapping problem, where "virtual" components are mapped into "real" components from pre-defined libraries to minimize an objective function while guaranteeing that system requirements are satisfied. ArchEx leverages an extensible set of patterns to enable formal, yet flexible, requirement specification, a graph-based internal representation of the system architecture, and algorithms based on mixed integer linear programming to solve the mapping problem. Its effectiveness is demonstrated on two industrial case studies: an aircraft power distribution network and a reconfigurable automated production line. Dmitrii Kirov, Pierluigi Nuzzo 0002, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 2017 | Optimized Design of a Human Intranet NetworkabstractWe address the design space exploration of wireless body area networks for wearable and implantable technologies, a task that is increasingly challenging as the number and variety of devices per person grow. Our method efficiently decomposes the problem into smaller subproblems by coordinating specialized analysis and optimization techniques. We leverage mixed integer linear programming to generate candidate network configurations based on coarse energy estimations. Accurate discrete-event simulation is used to check the feasibility of the proposed configurations under reliability constraints and guide the search to achieve fast convergence. Numerical results show that our application-specific approach substantially reduces the exploration time with respect to generic optimization techniques and helps provide clear identification of promising solutions. Ali Moin, Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Jan M. Rabaey |
DAC | 3 |
| 2017 | SMC: Satisfiability Modulo Convex OptimizationabstractWe address the problem of determining the satisfiability of a Boolean combination of convex constraints over the real numbers, which is common in the context of hybrid system verification and control. We first show that a special type of logic formulas, termed monotone Satisfiability Modulo Convex (SMC) formulas, is the most general class of formulas over Boolean and nonlinear real predicates that reduce to convex programs for any satisfying assignment of the Boolean variables. For this class of formulas, we develop a new satisfiability modulo convex optimization procedure that uses a lazy combination of SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. Our approach can then leverage the efficiency and the formal guarantees of state-of-the-art algorithms in both the Boolean and convex analysis domains. A key step in lazy satisfiability solving is the generation of succinct infeasibility proofs that can support conflict-driven learning and decrease the number of iterations between the SAT and the theory solver. For this purpose, we propose a suite of algorithms that can trade complexity with the minimality of the generated infeasibility certificates. Remarkably, we show that a minimal infeasibility certificate can be generated by simply solving one convex program for a sub-class of SMC formulas, namely ordered positive unate SMC formulas, that have additional monotonicity properties. Perhaps surprisingly, ordered positive unate formulas appear themselves very frequently in a variety of practical applications. By exploiting the properties of monotone SMC formulas, we can then build and demonstrate effective and scalable decision procedures for problems in hybrid system verification and control, including secure state estimation and robotic motion planning. Yasser Shoukry, Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, Paulo Tabuada |
HSCC | 3 |
| 2017 | Stochastic contracts for cyber-physical system design under probabilistic requirementsabstractWe develop an assume-guarantee contract framework for the design of cyber-physical systems, modeled as closed-loop control systems, under probabilistic requirements. We use a variant of signal temporal logic, namely, Stochastic Signal Temporal Logic (StSTL) to specify system behaviors as well as contract assumptions and guarantees, thus enabling automatic reasoning about requirements of stochastic systems. Given a stochastic linear system representation and a set of requirements captured by bounded StSTL contracts, we propose algorithms that can check contract compatibility, consistency, and refinement, and generate a controller to guarantee that a contract is satisfied, following a stochastic model predictive control approach. Our algorithms leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce both sound and tractable problem formulations. We illustrate the effectiveness of our approach on a few examples, including the design of embedded controllers for aircraft power distribution networks. Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Yugeng Xi 0001, Dewei Li 0001 |
MEMOCODE | 3 |
| 2016 | Diagnosis and Repair for Synthesis from Signal Temporal Logic SpecificationsabstractWe address the problem of diagnosing and repairing specifications for hybrid systems, formalized in signal temporal logic (STL). Our focus is on automatic synthesis of controllers from specifications using model predictive control. We build on recent approaches that reduce the controller synthesis problem to solving one or more mixed integer linear programs (MILPs), where infeasibility of an MILP usually indicates unrealizability of the controller synthesis problem. Given an infeasible STL synthesis problem, we present algorithms that provide feedback on the reasons for unrealizability, and suggestions for making it realizable. Our algorithms are sound and complete relative to the synthesis algorithm, i.e., they provide a diagnosis that makes the synthesis problem infeasible, and always terminate with a non-trivial specification that is feasible using the chosen synthesis method, when such a solution exists. We demonstrate the effectiveness of our approach on controller synthesis for various cyber-physical systems, including an autonomous driving application and an aircraft electric power system. Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo 0002, Vasumathi Raman, Alexandre Donzé, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, Sanjit A. Seshia |
HSCC | 6 |
| 2016 | The ultimate IoT application: A cyber-physical system for ambient assisted livingabstractWe propose a novel approach that integrates wireless, non-invasive devices with fast, real-time algorithms for large data analysis and biofeedback reaction, to discern the voluntariness of human movement through direct sensing of brain potentials combined with muscular action signal monitoring. The system has been tested in real situations. Daniela De Venuto, Valerio F. Annese, Alberto L. Sangiovanni-Vincentelli |
ISCAS | 3 |
| 2015 | Optimized selection of reliable and cost-effective cyber-physical system architectures
Nikunj Bajaj, Pierluigi Nuzzo 0002, Michael Masin, Alberto L. Sangiovanni-Vincentelli |
DATE | 4 |
| 2015 | A Mixed Discrete-Continuous Optimization Scheme for Cyber-Physical System Architecture ExplorationabstractWe propose a methodology for architecture exploration for Cyber-Physical Systems (CPS) based on an iterative, optimization-based approach, where a discrete architecture selection engine is placed in a loop with a continuous sizing engine. The discrete optimization routine proposes a candidate architecture to the sizing engine. The sizing routine optimizes over the continuous parameters using simulation to evaluate the physical models and to monitor the requirements. To decrease the number of simulations, we show how balance equations and conservation laws can be leveraged to prune the discrete space, thus achieving significant reduction in the overall runtime. We demonstrate the effectiveness of our methodology on an industrial case study, namely an aircraft environmental control system, showing more than one order of magnitude reduction in optimization time. John B. Finn, Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 2015 | Buildings to Grid Integration: A Dynamic Contract Approach
Mehdi Maasoumy, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 2015 | Let's get physical: Adding physical dimensions to cyber systemsabstractTechnology advances are creating major shifts in the industrial landscape. Traditional sectors such as transportation, medical and avionics, are witnessing fundamental changes in the supply chain and in the content where the interactions between the physical world and the computing world are becoming increasingly tight. Cyber Physical Systems, Systems of Systems, Internet of Things, Industrie 4.0, Swarm Systems and The Fog are all sectors that attract massive attention from the research communities and massive investment from industry. These concepts are tightly intertwined and describe a movement towards a fully interconnected planet where billions of devices interact via a complex mesh of wireless and wired communication infrastructures. The most compelling vision for the future of technology and industry is one where a swarm of devices is connected with the cloud to provide platforms for myriad of new applications. In this new world, new companies will arise and established ones will have to change radically their business model. The increasing sophistication and heterogeneity of these systems requires radical changes in the way sense-and-control platforms are designed to regulate them. In this presentation, I highlight some of the design challenges due to the complexity, heterogeneity and power consumption of CPS. Indeed, low power consumption is an essential requirement for the swarm of devices especially in the domain of wearable devices for healthcare. Coupled with low cost and reliability, power consumption has to be taken into consideration for any CPS deployment. Alberto L. Sangiovanni-Vincentelli |
ISLPED | 1 |
| 2015 | Design Automation of Electronic Systems: Past Accomplishments and Challenges Ahead [Scanning the Issue]abstractThe articles in this special issue provides an overview of and a perspective on the evolution of electronic design automation (EDA), and offers a perspective on some of the principal avenues of future development. Robert K. Brayton, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli, Tiziano Villa |
Proc. IEEE | 3 |
| 2015 | A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical SystemsabstractWe introduce a platform-based design methodology that uses contracts to specify and abstract the components of a cyber-physical system (CPS), and provide formal support to the entire CPS design flow. The design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. We review formalisms and tools that can be used to specify, analyze, or synthesize the design at different levels of abstraction. For each level, we highlight how the contract operations can be concretely computed as well as the research challenges that should be faced to fully implement them. We illustrate our approach on the design of embedded controllers for aircraft electric power distribution systems. Pierluigi Nuzzo 0002, Alberto L. Sangiovanni-Vincentelli, Davide Bresolin, Luca Geretti, Tiziano Villa |
Proc. IEEE | 2 |
| 2015 | Efficient Wire Routing and Wire Sizing for Weight Minimization of Automotive SystemsabstractAs the complexities of automotive systems increase, designing a system is a difficult task that cannot be done manually. In this paper, we focus on wire routing and wire sizing for weight minimization to deal with more and more connections between devices in automotive systems. The wire routing problem is formulated as a minimal Steiner tree problem with capacity constraints, and the location of a Steiner vertex is selected to add a splice which is used to connect more than two wires. We modify the Kou-Markowsky-Berman algorithm to efficiently construct Steiner trees and propose an integer linear programming (ILP) formulation to relocate Steiner vertices and satisfy capacity constraints. The ILP formulation is relaxed to a linear programming (LP) formulation which has the same optimal objective and can be solved more efficiently. Besides wire routing, wire sizing is also performed to satisfy resistance constraints and minimize the total wiring weight. To the best of our knowledge, this is the first work in the literature to formulate the automotive routing problem as a minimal Steiner tree problem with capacity constraints and perform wire routing and wire sizing for weight minimization. An industrial case study shows the effectiveness and efficiency of our algorithm which provides an efficient, flexible, and scalable approach for the design optimization of automotive systems. Chung-Wei Lin, Lei Rao, Paolo Giusto, Joseph D'Ambrosio, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 5 |
| 2015 | Security-Aware Design Methodology and Optimization for Automotive SystemsabstractIn this article, we address both security and safety requirements and solve security-aware design problems for the controller area network (CAN) protocol and time division multiple access (TDMA)-based protocols. To provide insights and guidelines for other similar security problems with limited resources and strict timing constraints, we propose a general security-aware design methodology to address security with other design constraints in a holistic framework and optimize design objectives. The security-aware design methodology is further applied to solve a security-aware design problem for vehicle-to-vehicle (V2V) communications with dedicated short-range communication (DSRC) technology. Experimental results demonstrate the effectiveness of our approaches in system design without violating design constraints and indicate that it is necessary to consider security together with other metrics during design stages. Chung-Wei Lin, Bowen Zheng 0001, Qi Zhu 0002, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Design Autom. Electr. Syst. | 4 |
| 2014 | An Efficient Wire Routing and Wire Sizing Algorithm for Weight Minimization of Automotive SystemsabstractAs the complexities of automotive systems increase, designing a system is a difficult task that cannot be done manually. In this paper, we propose an algorithm for weight minimization of wires used for connecting electronic devices in a system. The wire routing problem is formulated as a Steiner tree problem with capacity constraints, and the location of a Steiner vertex is selected for adding a splice connecting more than two wires. Besides wire routing, wire sizing is also done to satisfy resistance constraints and minimize the total wiring weight. Experimental results show the effectiveness and efficiency of our algorithm. Chung-Wei Lin, Lei Rao, Paolo Giusto, Joseph D'Ambrosio, Alberto L. Sangiovanni-Vincentelli |
DAC | 5 |
| 2014 | Library-based scalable refinement checking for contract-based designabstractGiven a global specification contract and a system described by a composition of contracts, system verification reduces to checking that the composite contract refines the specification contract, i.e. that any implementation of the composite contract implements the specification contract and is able to operate in any environment admitted by it. Contracts are captured using high-level declarative languages, for example, linear temporal logic (LTL). In this case, refinement checking reduces to an LTL satisfiability checking problem, which can be very expensive to solve for large composite contracts. This paper proposes a scalable refinement checking approach that relies on a library of contracts and local refinement assertions. We propose an algorithm that, given such a library, breaks down the refinement checking problem into multiple successive refinement checks, each of smaller scale. We illustrate the benefits of the approach on an industrial case study of an aircraft electric power system, with up to two orders of magnitude improvement in terms of execution time. Antonio Iannopollo, Pierluigi Nuzzo 0002, Stavros Tripakis, Alberto L. Sangiovanni-Vincentelli |
DATE | 4 |
| 2014 | Contract-based design of control protocols for safety-critical cyber-physical systemsabstractWe introduce a platform-based design methodology that addresses the complexity and heterogeneity of cyber-physical systems by using assume-guarantee contracts to formalize the design process and enable realization of control protocols in a hierarchical and compositional manner. Given the architecture of the physical plant to be controlled, the design is carried out as a sequence of refinement steps from an initial specification to a final implementation, including synthesis from requirements and mapping of higher-level functional and nonfunctional models into a set of candidate solutions built out of a library of components at the lower level. Initial top-level requirements are captured as contracts and expressed using linear temporal logic (LTL) and signal temporal logic (STL) formulas to enable requirement analysis and early detection of inconsistencies. Requirements are then refined into a controller architecture by combining reactive synthesis steps from LTL specifications with simulation-based design space exploration steps. We demonstrate our approach on the design of embedded controllers for aircraft electric power distribution. Pierluigi Nuzzo 0002, John B. Finn, Antonio Iannopollo, Alberto L. Sangiovanni-Vincentelli |
DATE | 4 |
| 2014 | Robust strategy synthesis for probabilistic systems applied to risk-limiting renewable-energy pricingabstractWe address the problem of synthesizing control strategies for Ellipsoidal Markov Decision Processes (EMDP), i.e., MDPs whose transition probabilities are expressed using ellipsoidal uncertainty sets. The synthesized strategy aims to maximize the total expected reward of the EMDP, constrained to a specification expressed in Probabilistic Computation Tree Logic (PCTL). We prove that the EMDP strategy synthesis problem for the fragment of PCTL disabling operators with a finite time bound is NP-complete and propose a novel sound and complete algorithm to solve it. Alberto Puggelli, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
EMSOFT | 2 |
| 2014 | Security-aware mapping for TDMA-based real-time distributed systemsabstractCyber-security has become a critical issue for realtime distributed embedded systems in domains such as automotive, avionics, and industrial automation. However, in many of such systems, tight resource constraints and strict timing requirements make it difficult or even impossible to add security mechanisms after the initial design stages. To produce secure and safe systems with desired performance, security must be considered together with other objectives at the system level and from the beginning of the design. In this paper, we focus on security-aware design for Time Division Multiple Access (TDMA) based real-time distributed systems. The TDMA-based protocol we consider is an abstraction of many time-triggered protocols that are being adopted in various safety-critical systems for their more predictable timing behavior, such as FlexRay, Time-Triggered Protocol, and Time-Triggered Ethernet. To protect against attacks on TDMA-based real-time distributed systems, we apply a message authentication mechanism with time-delayed release of keys, which provides a good balance between security and computational overhead but needs sophisticated network scheduling to ensure that the increased latencies due to delayed key releases will not violate timing requirements. We propose formulations and an algorithm to optimize the task allocation, priority assignment, network scheduling, and key-release interval length during the mapping process, while meeting both security and timing requirements. Experimental results of an automotive case study and a synthetic example show the effectiveness and efficiency of our approach. Chung-Wei Lin, Qi Zhu 0002, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 2014 | Are interface theories equivalent to contract theories?abstractContract-based design is emerging as a unifying compositional paradigm for the specification, design and verification of large-scale complex systems. Different contract frameworks are currently available, but we lack a clear understanding of the relations between them. In this paper, we investigate the relation between interface theories (specifically, relational interfaces) and assume-guarantee (A/G) contracts. We introduce a natural transformation of interfaces to A/G contracts represented by linear temporal logic. Then, we analyze differences and correspondences between key operators and relations in the two theories (i.e. composition, refinement and conjunction), by studying their preservation properties under the proposed transformation. We show that the transformation preserves refinement, but does not generally preserve serial composition and conjunction. Then, we present an assumption-projection operator to make it possible to preserve serial composition and compatibility checking. Finally, we provide illustrative examples that shed light on the effectiveness of both frameworks for requirement formalization, early detection of integration errors, and use of abstraction-refinement. Pierluigi Nuzzo 0002, Antonio Iannopollo, Stavros Tripakis, Alberto L. Sangiovanni-Vincentelli |
MEMOCODE | 4 |
| 2014 | An MDA Approach for the Generation of Communication Adapters Integrating SW and FW Components from Simulink
Marco Di Natale, Francesco Chirico, Andrea Sindico, Alberto L. Sangiovanni-Vincentelli |
MoDELS | 4 |
| 2014 | Optimized implementation of synchronous models on industrial LTTA systems
Marco Di Natale, Qi Zhu 0002, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis |
J. Syst. Archit. | 3 |
| 2013 | Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
Alberto Puggelli, Wenchao Li 0001, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
CAV | 3 |
| 2013 | Panel: the heritage of Mead & Conway: what has remained the same, what was missed, what has changed, what lies ahead
Marco Casale-Rossi, Alberto L. Sangiovanni-Vincentelli, Luca P. Carloni, Bernard Courtois, Hugo De Man, Antun Domic, Jan M. Rabaey |
DATE | 2 |
| 2013 | Dr. Frankenstein's dream made possible: implanted electronic devicesabstractThe developments in micro-nano-electronics, biology and neuro-sciences make it possible to imagine a new world where vital signs can be monitored continuously, artificial organs can be implanted in human bodies and interfaces between the human brain and the environment can extend the capabilities of men thus making the dream of Dr. Frankenstein become true. This paper surveys some of the most innovative implantable devices and offers some perspectives on the ethical issues that come with the introduction of this technology. Daniela De Venuto, Alberto L. Sangiovanni-Vincentelli |
DATE | 2 |
| 2013 | BAG: a designer-oriented integrated framework for the development of AMS circuit generatorsabstractWe introduce BAG, the Berkeley Analog Generator, an integrated framework for the development of generators of Analog and Mixed Signal (AMS) circuits. Such generators are parameterized design procedures that produce sized schematics and correct layouts optimized to meet a set of input specifications. BAG extends previous work by implementing interfaces to integrate all steps of the design flow into a single environment and by providing helper classes - both at the schematic and layout level - to aid the designer in developing truly parameterized and technology-independent circuit generators. This simplifies the codification of common tasks including technology characterization, schematic and testbench translation, simulator interfacing, physical verification and extraction, and parameterized layout creation for common styles of layout. We believe that this approach will foster design reuse, ease technology migration, and shorten time-to-market, while remaining close to the classical design flow to ease adoption. We have used BAG to design generators for several circuits, including a Voltage Controlled Oscillator (VCO) and a Switched-Capacitor (SC) voltage regulator in a CMOS 65nm process. We also present results from automatic migration of our designs to a 40nm process. John Crossley, Alberto Puggelli, Hanh-Phuc Le, R. Nancollas, Kwangmo Jung, Nathan Narevsky, Yue Lu 0007, Nicholas Sutardja, E. J. An, Alberto L. Sangiovanni-Vincentelli, Elad Alon |
ICCAD | 12 |
| 2013 | Security-aware mapping for CAN-based real-time distributed automotive systemsabstractCyber-security is a rising issue for automotive electronic systems, and it is critical to system safety and dependability. Current in-vehicles architectures, such as those based on the Controller Area Network (CAN), do not provide direct support for secure communications. When retrofitting these architectures with security mechanisms, a major challenge is to ensure that system safety will not be hindered, given the limited computation and communication resources. We apply Message Authentication Codes (MACs) to protect against masquerade and replay attacks on CAN networks, and propose an optimal Mixed Integer Linear Programming (MILP) formulation for solving the mapping problem from a functional model to the CAN-based platform while meeting both the security and the safety requirements. We also develop an efficient heuristic for the mapping problem under security and safety constraints. To the best of our knowledge, this is the first work to address security and safety in an integrated formulation in the design automation of automotive electronic systems. Experimental results of an industrial case study show the effectiveness of our approach. Chung-Wei Lin, Qi Zhu 0002, Calvin Phung, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 2013 | Timing analysis of process graphs with finite communication buffersabstractReal-Time Calculus (RTC) is a modular performance analysis framework for real-time embedded systems. It can be used to compute the worst-case and best-case response times of tasks with general activation patterns and configurations, such as pipelines of tasks that are connected via finite buffers. In this paper, we extend the existing RTC framework to analyze arbitrary graph configurations of tasks and messages, with mixed periodic and event-based activation models and finite buffers between any pair of nodes. Our extension also improves upon several sources of pessimism in the existing analysis. We present an application of the extended RTC to the Loosely Time-Triggered Architecture (LTTA) implementation of synchronous models, commonly used in the development of embedded automotive, avionics and control systems. We show how our method can be used to model scheduling and communication delays in an LTTA mapping, which gives tighter analysis bounds on the output rate and the latency compared to existing techniques. The evaluation on automotive workloads shows that our approach is scalable and outperforms existing techniques in terms of analysis accuracy. Chung-Wei Lin, Marco Di Natale, Haibo Zeng 0001, Linli Thi Xuan Phan, Alberto L. Sangiovanni-Vincentelli |
IEEE Real-Time and Embedded Technology and Applications Symposium | 5 |
| 2013 | metroII: A design environment for cyber-physical systemsabstractCyber-Physical Systems are integrations of computation and physical processes and as such, will be increasingly relevant to industry and people. The complexity of designing CPS resides in their heterogeneity. Heterogeneity manifest itself in modeling their functionality as well as in the implementation platforms that include a multiplicity of components such as microprocessors, signal processors, peripherals, memories, sensors and actuators often integrated on a single chip or on a small package such as a multi-chip module. We need a methodology, tools and environments where heterogeneity can be dealt with at all levels of abstraction and where different tools can be integrated. We present here Platform-Based Design as the CPS methodology of choice and metro II, a design environment that supports it. We present the metamodeling approach followed in metro II, how to couple the functionality and implementation platforms of CPS, and the simulation technology that supports the analysis of CPS and of their implementation. We also present examples of use and the integration of metro II with another popular design environment developed at Verimag, BIP. Abhijit Davare, Douglas Densmore, Liangpeng Guo, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli, Alena Simalatsar, Qi Zhu 0002 |
ACM Trans. Embed. Comput. Syst. | 5 |
| 2013 | Duty-cycle optimization for IEEE 802.15.4 wireless sensor networksabstractMost applications of wireless sensor networks require reliable and timely data communication with maximum possible network lifetime under low traffic regime. These requirements are very critical especially for the stability of wireless sensor and actuator networks. Designing a protocol that satisfies these requirements in a network consisting of sensor nodes with traffic pattern and location varying over time and space is a challenging task. We propose an adaptive optimal duty-cycle algorithm running on top of the IEEE 802.15.4 medium access control to minimize power consumption while meeting the reliability and delay requirements. Such a problem is complicated because simple and accurate models of the effects of the duty cycle on reliability, delay, and power consumption are not available. Moreover, the scarce computational resources of the devices and the lack of prior information about the topology make it impossible to compute the optimal parameters of the protocols. Based on an experimental implementation, we propose simple experimental models to expose the dependency of reliability, delay, and power consumption on the duty cycle at the node and validate it through extensive experiments. The coefficients of the experimental-based models can be easily computed on existing IEEE 802.15.4 hardware platforms by introducing a learning phase without any explicit information about data traffic, network topology, and medium access control parameters. The experimental-based model is then used to derive a distributed adaptive algorithm for minimizing the power consumption while meeting the reliability and delay requirements in the packet transmission. The algorithm is easily implementable on top of the IEEE 802.15.4 medium access control without any modifications of the protocol. An experimental implementation of the distributed adaptive algorithm on a test bed with off-the-shelf wireless sensor devices is presented. The experimental performance of the algorithms is compared to the existing solutions from the literature. The experimental results show that the experimental-based model is accurate and that the proposed adaptive algorithm attains the optimal value of the duty cycle, maximizing the lifetime of the network while meeting the reliability and delay constraints under both stationary and transient conditions. Specifically, even if the number of devices and their traffic configuration change sharply, the proposed adaptive algorithm allows the network to operate close to its optimal value. Furthermore, for Poisson arrivals, the duty-cycle protocol is modeled as a finite capacity queuing system in a star network. This simple analytical model provides insights into the performance metrics, including the reliability, average delay, and average power consumption of the duty-cycle protocol. Pan Gun Park, Sinem Coleri Ergen, Carlo Fischione, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Sens. Networks | 4 |
| 2012 | An Industrial System Engineering Process Integrating Model Driven Architecture and Model Based Design
Andrea Sindico, Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
MoDELS | 3 |
| 2012 | Modeling Cyber-Physical SystemsabstractThis paper focuses on the challenges of modeling cyber–physical systems (CPSs) that arise from the intrinsic heterogeneity, concurrency, and sensitivity to timing of such systems. It uses a portion of an aircraft vehicle management system (VMS), specifically the fuel management subsystem, to illustrate the challenges, and then discusses technologies that at least partially address the challenges. Specific technologies described include hybrid system modeling and simulation, concurrent and heterogeneous models of computation, the use of domain-specific ontologies to enhance modularity, and the joint modeling of functionality and implementation architectures. Patricia Derler, Edward A. Lee, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 3 |
| 2012 | Separate compilation of hierarchical real-time programs into linear-bounded Embedded Machine code
Arkadeb Ghosal, Daniel T. Iercan, Christoph M. Kirsch, Thomas A. Henzinger, Alberto L. Sangiovanni-Vincentelli |
Sci. Comput. Program. | 5 |
| 2012 | Optimization of task allocation and priority assignment in hard real-time distributed systemsabstractThe complexity and physical distribution of modern active safety, chassis, and powertrain automotive applications requires the use of distributed architectures. Complex functions designed as networks of function blocks exchanging signal information are deployed onto the physical HW and implemented in a SW architecture consisting of a set of tasks and messages. The typical configuration features priority-based scheduling of tasks and messages and imposes end-to-end deadlines. In this work, we present and compare formulations and procedures for the optimization of the task allocation, the signal to message mapping, and the assignment of priorities to tasks and messages in order to meet end-to-end deadline constraints and minimize latencies. Our formulations leverage worst-case response time analysis within a mixed integer linear optimization framework and are compared for performance against a simulated annealing implementation. The methods are applied for evaluation to an automotive case study of complexity comparable to industrial design problems. Qi Zhu 0002, Haibo Zeng 0001, Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Embed. Comput. Syst. | 5 |
| 2011 | Are logic synthesis tools robust?abstractA systematic investigation is presented about the robustness of logic synthesis tools to equivalence-preserving transformations of the input Verilog file. We have developed a framework that: 1) parses Verilog behavioral models into an abstract syntax tree; 2) generates random equivalence-preserving transformations on the syntax tree, and; 3) writes the transformed design back in Verilog format. The original and the transformed Verilog descriptions are then checked for equivalence and synthesized. Results show that average (peak) improvements in area of 2.5% (11%) and length of the critical path of 4% (13%) are achievable. Indeed these figures are comparable to recent advancements in logic synthesis ([17] [8] achieve 4.9% (23%) 5% (24%) improvements area-wise, respectively), signaling a relevant lack of robustness in synthesis tools. This lack of robustness suggests that new synthesis algorithms should be evaluated by measuring the average improvement on several transformed files to assess their real contributions to the quality of the results. Alberto Puggelli, Tobias Welp, Andreas Kuehlmann, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 2011 | Component-based design for the futureabstractAll in-text\treferences\tunderlined\tin\tblue\tare\tlinked\tto\tpublications\ton\tResearchGate, letting you\taccess\tand\tread\tthem\timmediately. Edward A. Lee, Alberto L. Sangiovanni-Vincentelli |
DATE | 2 |
| 2011 | Schedule Optimization of Time-Triggered Systems Communicating Over the FlexRay Static SegmentabstractFlexRay is a new high-bandwidth communication protocol for the automotive domain, providing support for the transmission of time-critical periodic frames in a static segment and priority-based scheduling of event-triggered frames in a dynamic segment. The design of a system scheduling with communication over the FlexRay static segment is not an easy task because of protocol constraints and the demand for extensibility and flexibility. We study the problem of the ECU and FlexRay bus scheduling synthesis from the perspective of the application designer, interested in optimizing the scheduling subject to timing constraints with respect to latency- or extensibility-related metric functions. We provide solutions for a task and signal scheduling problem, including different task scheduling policies based on existing industry standards. The solutions are based on the Mixed-Integer Linear Programming optimization framework. We show the results of the application of the method to case studies consisting of an X-by-wire system on actual prototype vehicles. Haibo Zeng 0001, Marco Di Natale, Arkadeb Ghosal, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 4 |
| 2011 | Breath: An Adaptive Protocol for Industrial Control Applications Using Wireless Sensor NetworksabstractAn energy-efficient, reliable and timely data transmission is essential for Wireless Sensor Networks (WSNs) employed in scenarios where plant information must be available for control applications. To reach a maximum efficiency, cross-layer interaction is a major design paradigm to exploit the complex interaction among the layers of the protocol stack. This is challenging because latency, reliability, and energy are at odds, and resource-constrained nodes support only simple algorithms. In this paper, the novel protocol Breath is proposed for control applications. Breath is designed for WSNs where nodes attached to plants must transmit information via multihop routing to a sink. Breath ensures a desired packet delivery and delay probabilities while minimizing the energy consumption of the network. The protocol is based on randomized routing, medium access control, and duty-cycling jointly optimized for energy efficiency. The design approach relies on a constrained optimization problem, whereby the objective function is the energy consumption and the constraints are the packet reliability and delay. The challenging part is the modeling of the interactions among the layers by simple expressions of adequate accuracy, which are then used for the optimization by in-network processing. The optimal working point of the protocol is achieved by a simple algorithm, which adapts to traffic variations and channel conditions with negligible overhead. The protocol has been implemented and experimentally evaluated on a testbed with off-the-shelf wireless sensor nodes, and it has been compared with a standard IEEE 802.15.4 solution. Analytical and experimental results show that Breath is tunable and meets reliability and delay requirements. Breath exhibits a good distribution of the working load, thus ensuring a long lifetime of the network. Therefore, Breath is a good candidate for efficient, reliable, and timely data gathering for control applications. Pan Gun Park, Carlo Fischione, Alvise Bonivento, Karl Henrik Johansson, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Mob. Comput. | 5 |
| 2010 | Education panel: designing the always connected car of the futureabstractThe automotive industry is introducing novel features, such as seamless vehicle-to-vehicle and vehicle-to-infrastructure connectivity to improve in vehicle driver safety (e.g., forward collision warnings) and comfort (e.g., routing to avoid congestion) while facing stricter government regulations, and shortened time-to-markets. As a result, automotive Electronic Control System (ECS) architectures are becoming increasingly complex. To cope with these challenges and opportunities, the entire automotive supply chain is engaged as follows: automotive OEMs are managing complexity by reusing legacy components and enabling new technologies; tier one suppliers are increasingly up-integrating features on the same computing platform; tier two suppliers are providing multi-core and other powerful technologies; academic institutions are doing research in new analysis, synthesis and optimization methods; and tool providers are trying to raise the level of abstraction for system modeling, analysis and optimization. The panel will address the following topics: Arkadeb Ghosal, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli, Joseph D'Ambrosio, Ed Nuckolls, Harald Wilhelm, Jim Tung, Markus Kuhl, Peter van Staa |
DAC | 3 |
| 2010 | All things are connectedabstractSummary form only given. Design of complex system is essentially about connections: Connection of concepts, connection of objects, connection of teams. And products of the future will be connected seamlessly across physical and virtual domains. Connections can produce systems that offer more than the sum of the components but they can also yield to systems that are less powerful than the sum of the components or that are so compromised by their interactions that they do not work at all. Collaboration is the name of the game for design, for production, for operation of multi-scale systems. There is increasingly less distance between design and operation of systems. An efficient management of interactions among deployed parts of a larger system requires principles that are common to the design methods developed at the bleeding edge of technology. I will examine the evolution of design principles and of multiscale systems and the challenges we are facing today. I will point to a number of exciting fields where advances are constantly made towards the mastering of connections. Alberto L. Sangiovanni-Vincentelli |
DATE | 1 |
| 2010 | CalCS: SMT solving for non-linear convex constraints
Pierluigi Nuzzo 0002, Alberto Puggelli, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli |
FMCAD | 4 |
| 2010 | A 2.2mW CMOS LNA for 6-8.5GHz UWB receiversabstractThis paper presents an ultra-wideband (UWB) low noise amplifier (LNA) consuming 2.2-mW core dc power for 6-8.5GHz wireless applications. A common-gate input stage is cascaded with a common-source second stage to perform input impedance matching and wideband stagger-tuning amplification, while the current-reuse topology minimizes the dc power dissipation. The design method used to achieve flat-gain response is presented. A detailed analysis gives insight into the issue on the input impedance and suggests a solution. Implemented in a 90-nm CMOS process, the measurement results show power gain of 13.35+/-0.55 dB, input third intercept point (IIP3) of-6.2 dBm, and noise figure of 5-6.5 dB. The silicon die with 0.22-mm2active area allows the design to be adopted for highly integrated low-cost CMOS applications. Chang-Ching Wu, Xuening Sun, Alberto L. Sangiovanni-Vincentelli, Jan M. Rabaey |
ISCAS | 3 |
| 2010 | A Design Flow for Building Automation and Control SystemsabstractWe propose a system-level design flow for building automation and control (BAC) systems. The input to the design flow is a high level description of the control algorithms given in a model-based environment such as Simulink. The input specification is translated into an intermediate format, and then automatically refined into a distributed implementation. Refinement includes optimal mapping of the functional specification on a set of computation and communication resources, and software synthesis, which generates code for each component in the mapped design while guaranteeing semantic equivalence with the original specification. Experiments with a temperature control system are presented to illustrate the flow. Yang Yang 0040, Alessandro Pinto, Alberto L. Sangiovanni-Vincentelli, Qi Zhu 0002 |
RTSS | 3 |
| 2010 | Moving From Federated to Integrated Architectures in Automotive: The Role of Standards, Methods and ToolsabstractCost pressure, flexibility, extensibility and the need for coping with increased functional complexity are changing the fundamental paradigms for the definition of automotive and aeronautics architectures. Traditional designs are based on the concept of aFederated Architecturein which integrated hardware/software components [Electronic Control Units (ECUs)] realize mostly independent or loosely interconnected functions. These components are connected by bus and cooperate by exchanging messages. This paradigm is now being replaced by theIntegrated Architecture,—the concept comes from Integrated Modular Avionics (IMA) introduced by the avionics community (see C. B. Watkins and R. Walter, “Transitioning from federated avionics architectures to integrated modular avionics,” in Proc. 26th Digital Avionics Syst. Conf., Oct. 2007) but it is certainly general and applicable to other fields and in particular, automotive—in which software components can be supplied from multiple sources, integrated on the same hardware platform or physically distributed and possibly moved from one CPU to another without loss of functional and time correctness and providing a guaranteed level of reliability. This shift will decouple software design from the hardware platform design and provide opportunities for the optimization of the architecture configuration, increased extensibility, flexibility and modularity. However, the integration of software components in a distributed system realizing a complex functional behavior and characterized by safety, time and reliability constraints requires a much tighter control on the component model and its semantics, new methods and tools for analyzing the results of the composition, whether by simulation or formal methods, and methods for exploring the architecture solution space and optimizing the configuration. We provide a general overview of existing challenges and possible solutions to the design and analysis problem,with special focus on the automotive domain. The development of such methods and tools must necessarily consider compatibility with existing modeling languages and standards, including UML, AUTOSAR and synchronous reactive models, on which the widely used commercial products Simulink and SCADE are based. Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 2 |
| 2010 | Synthesis of Multi-task Implementations of Simulink Models with Minimum DelaysabstractModel-based design of embedded control systems using Synchronous Reactive (SR) models is among the best practices for software development in the automotive and aeronautic industry. SR models allow to formally verify the correctness of the design and automatically generate the implementation code. This feature is a major productivity enhancement and, more importantly, can ensure correct-by-design software provided that the code generator is provably correct. This paper presents an improvement of code generation technology for SR obtained via a novel algorithm for optimizing the multitask implementation of Simulink models on single-processor platforms with limited availability of memory. Existing code generation tools require the addition of zero-order hold (ZOH) blocks, and therefore additional memory, and possibly also additional functional delays whenever there is a rate transition in the computation and communication flow. Our algorithm leverages a novel efficient encoding of the scheduling feasibility region to find the task implementation of function blocks with minimum additional functional delays within timing and memory constraints. The algorithm is applied to an automotive case study with tens of function blocks and very high utilization to test its applicability to complex systems. Marco Di Natale, Liangpeng Guo, Haibo Zeng 0001, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 4 |
| 2010 | Optimal synthesis of communication procedures in real-time synchronous reactive modelsabstractModel-based design methodologies are gaining attention in the industrial community because of the possibility of early and efficient functional validation and formal verification of properties at high levels of abstraction. The advantages of validating the design using high-level models can be lost entirely if errors and modifications that are not back-annotated to the higher abstraction levels are introduced when refining the design to lower levels of abstraction. To overcome this problem and to reduce design time, automatic synthesis has been used for the refinement process from Register Transfer Languages (RTLs) to logic gates for digital circuit design. This approach guarantees (assuming that the synthesis algorithms are correctly implemented) that the semantic of the RTL description is semantically equivalent to the semantic of the logic circuit. Automatic code generation is similar in intent and applicability. However, the software implementation of the abstract model must make efficient use of the platform resources that may not reflect all the assumptions of the code generation algorithms. The implementation of communication in a synchronous reactive model requires buffering and access procedures at the kernel level. In previous work, we obtained tight bounds on the size of communication buffers to maintain semantic equivalence. In realtime systems, however, because of the longer execution times of access procedures, an implementation with minimum buffer size may lead to the violation of deadlines. To solve this problem, we propose a Mixed Integer Linear Programming (MILP)-based optimization approach that provides the minimum memory implementation of a set of communication channels while guaranteeing that the task deadline constraints are met. The analysis is validated by an OSEK/VDX-compliant implementation that provides an estimate of actual runtime overheads. The approach is applied to a set of task graphs and an automotive case study. Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 3 |
| 2010 | Using Statistical Methods to Compute the Probability Distribution of Message Response Time in Controller Area NetworkabstractAutomotive electrical/electronic (E/E) architectures need to be evaluated and selected based on the estimated performance of the functions deployed on them before the details of these functions are known. End-to-end delays of controls must be estimated using incomplete and aggregate information on the computation and communication load for ECUs and buses. We describe the use of statistical analysis to compute the probability distribution of Controller Area Network (CAN) message response times when only partial information is available about the functionality and architecture of a vehicle. We provide results compared to simulations as well as trace data. These results demonstrate that our statistical inference can be used for predicting the distribution of the response time of a CAN message, once its priority has been assigned, from limited information such as the bus utilization of higher priority messages. Haibo Zeng 0001, Marco Di Natale, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 4 |
| 2010 | Optimizing the Software Architecture for Extensibility in Hard Real-time Distributed SystemsabstractWe consider a set of control tasks that must be executed on distributed platforms so that end-to-end latencies are within deadlines. We investigate how to allocate tasks to nodes, pack signals to messages, allocate messages to buses, and assign priorities to tasks and messages, so that the design is extensible and robust with respect to changes in task requirements. We adopt a notion of extensibility metric that measures how much the execution times of tasks can be increased without violating end-to-end deadlines. We optimize the task and message design with respect to this metric by adopting a mathematical programming front-end followed by postprocessing heuristics. The proposed algorithm as applied to industrial strength test cases shows its effectiveness in optimizing extensibility and a marked improvement in running time with respect to an approach based on randomized optimization. Qi Zhu 0002, Yang Yang 0040, Marco Di Natale, Eelco Scholte, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 5 |
| 2009 | Contract-based system-level composition of analog circuitsabstractEfficient system-level design is increasingly relying on hierarchical design-space exploration, as well as compositional methods, to shorten time-to-market, leverage design re-use, and achieve optimal performances. However, in analog electronic systems, circuit behaviors are so tightly dependent on their interface conditions that accurate system performance estimations based on characterizations of individual stand-alone circuits is a hard task. Since there is no general solution to this problem, analog system integration has traditionally used ad-hoc solutions heavily dependent on designers' experience. In this paper, we build upon the analog platform-based design methodology by exploiting contracts to enforce correct-by-construction system-level composition. Contracts intuitively capture the thought process of a designer, who aims at guaranteeing circuit performance only under specific assumptions (e.g. loading and dynamic range) on the interface properties. Our approach allows automatic detection and composition of compatible components in a given library. We apply our methodology to an ultra-wide band receiver front-end to show that contracts allow pre-designed IP components to be smoothly integrated and design decisions to be reliably made at a higher abstraction level, both key factors to improve designer productivity. Xuening Sun, Pierluigi Nuzzo 0002, Chang-Ching Wu, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 2009 | Scheduling the FlexRay bus using optimization techniquesabstractFlexRay is a new communication protocol for automotive systems, providing support for transmission of periodic messages in static segments and priority-based scheduling of event-triggered messages in dynamic segments. The design of a FlexRay schedule is not an easy task because of protocol constraints and demands for extensibility and flexibility. We study the problem of FlexRay bus scheduling from the perspective of the application designer, interested in optimizing the performance of application related timing metrics or extensibility. We provide solutions for different task scheduling policies on existing industry standards based on a mixed integer linear programming (MILP) framework. Haibo Zeng 0001, Marco Di Natale, Arkadeb Ghosal, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli |
DAC | 6 |
| 2009 | UMTS MPSoC design evaluation using a system level design frameworkabstractRapid design space exploration with accurate models is necessary to improve designer productivity at the electronic system level. We describe how to use a new event-based design framework, Metro II, to carry out simulation and design space exploration of multi-core architectures. We illustrate the design methodology on a UMTS data link layer design case study with both a timed and untimed functional model as well as a complete set of MPSoC architectural services. We compare different architectures (including RTOSes) explored with Metro II and quantify the associated simulation overhead. Douglas Densmore, Alena Simalatsar, Abhijit Davare, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli |
DATE | 5 |
| 2009 | Optimizations of an application-level protocol for enhanced dependability in FlexRayabstractFlexRay [9] is an automotive standard for high-speed and reliable communication that is being widely deployed for next generation cars. The protocol has powerful error-detection mechanisms, but its error-management scheme forces a corrupted frame to be dropped without any notification to the transmitter. In this paper, we analyze the feasibility of and propose an optimization approach for an application-level acknowledgement and retransmission scheme for which transmission time is allocated on top of an existing schedule. We formulate the problem as a Mixed Integer Linear Program. The optimization is comprised of two stages. The first stage optimizes a fault tolerance metric; the second improves scheduling by minimizing the latencies of the acknowledgement and retransmission messages. We demonstrate the effectiveness of our approach on a case study based on an experimental vehicle designed at General Motors. Wenchao Li 0001, Marco Di Natale, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
DATE | 5 |
| 2009 | Iterative Node Deployment in an Unknown EnvironmentabstractWe consider the problem of deploying relay nodes to achieve connectivity with minimum cost in a sensor network of unknown radio propagation characteristics. For a network where a certain number of targets or sensing nodes have already been deployed in fixed and known positions, we aim at efficiently adding communication or relay nodes to guarantee connectivity with minimum cost, between any sensor node and a base station. The communication cost of a wireless link is defined as the expected number of retransmissions over that link and is modeled using an underlying Gaussian process (GP) between the nodes. We propose an iterative sensor deployment approach that learns the parameters of the underlying GP while deploying the additional nodes in the best positions possible at each step. Our deployment algorithm is more powerful with respect to the ones found in literature since: 1) we do not assume fixed communication range, i.e., we do not assume that nodes can perfectly communicate within a fixed range and will not communicate at all outside that range (this assumption is not realistic for the wireless channel); 2) we do not assume the existence of a pilot deployment aimed at learning the radio propagation characteristics because of the high cost of the deployment process and of the sensor nodes themselves. Assane Gueye, Sinem Coleri Ergen, Alberto L. Sangiovanni-Vincentelli |
GLOBECOM | 3 |
| 2009 | Peer-to-peer estimation over wireless sensor networks via Lipschitz optimization
Carlo Fischione, Alberto Speranzon, Karl Henrik Johansson, Alberto L. Sangiovanni-Vincentelli |
IPSN | 4 |
| 2009 | Optimizing Extensibility in Hard Real-Time Distributed SystemsabstractWe consider a set of control tasks that must be executed on distributed platforms so that end-to-end latencies are within deadlines. We investigate how to allocate tasks to nodes, pack signals to messages, allocate messages to buses, and assign priorities to tasks and messages, so that the design is robust with respect to changes in task requirements. The notion of extensibility is used to measure robustness. The extensibility metric measures how much the execution times of tasks can be increased without violating end-to-end deadlines. We optimize this metric by adopting a mathematical programming front-end followed by post-processing heuristics. The proposed algorithm as applied to industrial strength test cases shows its effectiveness in optimizing extensibility and a marked improvement in running time with respect to an approach based on randomized optimization. Qi Zhu 0002, Yang Yang 0040, Eelco Scholte, Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
IEEE Real-Time and Embedded Technology and Applications Symposium | 5 |
| 2009 | Medium Access Control Analytical Modeling and Optimization in Unslotted IEEE 802.15.4 Wireless Sensor NetworksabstractAccurate analytical expressions of delay and packet reception probabilities, and energy consumption of duty-cycled wireless sensor networks with random medium access control (MAC) are instrumental for the efficient design and optimization of these resource-constrained networks. Given a clustered network topology with unslotted IEEE 802.15.4 and preamble sampling MAC, a novel approach to the modeling of the delay, reliability, and energy consumption is proposed. The challenging part in such a modeling is the random MAC and sleep policy of the receivers, which prevents to establish the exact time of data packet transmission. The analysis gives expressions as function of sleep time, listening time, traffic rate and MAC parameters. The analytical results are then used to optimize the duty cycle of the nodes and MAC protocol parameters. The approach provides a significant reduction of the energy consumption compared to existing solutions in the literature. Monte Carlo simulations by ns2 assess the validity of the analysis. Carlo Fischione, Sinem Coleri Ergen, Pan Gun Park, Karl Henrik Johansson, Alberto L. Sangiovanni-Vincentelli |
SECON | 5 |
| 2009 | The Tire as an Intelligent SensorabstractActive safety systems are based upon the accurate and fast estimation of the value of important dynamical variables such as forces, load transfer, actual tire-road friction (kinetic friction) muk, and maximum tire-road friction available (potential friction) mup. Measuring these parameters directly from tires offers the potential for improving significantly the performance of active safety systems. We present a distributed architecture for a data-acquisition system that is based on a number of complex intelligent sensorsinsidethetirethat form a wireless sensor network with coordination nodes placed on the body of the car. The design of this system has been extremely challenging due to the very limited available energy combined with strict application requirements for data rate, delay, size, weight, and reliability in a highly dynamical environment. Moreover, it required expertise in multiple engineering disciplines, including control-system design, signal processing, integrated-circuit design, communications, real-time software design, antenna design, energy scavenging, and system assembly. Sinem Coleri Ergen, Alberto L. Sangiovanni-Vincentelli, Xuening Sun, Riccardo Tebano, S. Alalusi, G. Audisio, Marco Sabatini |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2009 | A Methodology for Constraint-Driven Synthesis of On-Chip CommunicationsabstractWe present a methodology and an optimization framework for the synthesis of on-chip communication through the assembly of components such as interfaces, routers, buses, and links, from a target library. Models for functionality, cost, and performance of each element are captured in the library together with their composition rules. We develop a mathematical framework to model communication at different levels of abstraction from the point-to-point input specification to the library elements and the final implementation. Alessandro Pinto, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2009 | Challenges and Solutions in the Development of Automotive SystemsabstractThis special section on automotive systems collects four of the presentations given on a special day at the DATE 08 Conference, held in Munich, Germany, in April 2008. Alberto L. Sangiovanni-Vincentelli, Marco Di Natale |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 2009 | Improving the size of communication buffers in synchronous models with time constraintsabstractModel-based development of embedded applications is a major trend in industry because of the possibility of early validation and verification of properties by simulation or formal methods. Synchronous reactive models are characterized by a formally specified semantics, which avoids ambiguities in the interpretation of the model, and by the availability of efficient code generation tools, which help increase productivity. The validity of the simulation and/or verification results on the model is retained only if the generated code is guaranteed to preserve model semantics. At the same time, the implementation must make efficient use of the execution platform resources. One of the essential issues for efficient implementation is the use of communication buffers that exploit the multirate behavior of the components. In most embedded devices, RAM memory is scarce and buffer size should be kept at a minimum. We present an approach to buffer size optimization by using timing information about the components. The approach was applied to an automotive case study, showing for the specific case an improvement of at least 7.5% with respect to previous methods. Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 3 |
| 2009 | Stochastic Analysis of Distributed Real-time Automotive SystemsabstractMany automotive applications, including most of those developed for active safety and chassis systems, must comply with hard real-time deadlines, and are also sensitive to the average latency of the end-to-end computations from sensors to actuators. A characterization of the timing behavior of functions is used to estimate the quality of an architecture configuration in the early stages of architecture selection. In this paper, we extend previous work on stochastic analysis of response times for software tasks to controller area network messages, then compose them with sampling delays to compute probability distributions of end-to-end latencies. We present the results of the analysis on a realistic complex distributed automotive system. The distributions predicted by our method are very close to the probability of latency values measured on a simulated system. However, the faster computation time of the stochastic analysis is much better suited to the architecture exploration process, allowing a much larger number of configurations to be analyzed and evaluated. Haibo Zeng 0001, Marco Di Natale, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 4 |
| 2009 | Minimum Energy coding in CDMA Wireless Sensor NetworksabstractA theoretical framework is proposed for accurate comparison of minimum energy coding in Coded Division Multiple Access (CDMA) Wireless Sensor Networks (WSNs). Energy consumption and reliability are analyzed for two coding schemes: Minimum Energy coding (ME), and Modified Minimum Energy coding (MME). A detailed model of consumed energy is described as function of the coding, radio transmit power, the characteristics of the transceivers, and the dynamics of the wireless channel. Since CDMA is strongly limited by multi-access interference, the system model includes all the relevant characteristics of wireless propagation. A distributed and asynchronous algorithm, which minimizes the total energy consumption by controlling the radio power, is developed. Numerical results are presented to validate the theoretical analysis and show under which conditions MME outperforms ME with respect to energy consumption and bit error rate. It is concluded that MME is more energy efficient than ME only for short codewords. Carlo Fischione, Karl Henrik Johansson, Alberto L. Sangiovanni-Vincentelli, Benigno Zurita Ares |
IEEE Trans. Wirel. Commun. | 3 |
| 2008 | Logical Reliability of Interacting Real-Time TasksabstractWe propose the notion of logical reliability for real-time program tasks that interact through periodically updated program variables. We describe a reliability analysis that checks if the given short-term (e.g., single-period) reliability of a program variable update in an implementation is sufficient to meet the logical reliability requirement (of the program variable) in the long run. We then present a notion of design by refinement where a task can be refined by another task that writes to program variables with less logical reliability. The resulting analysis can be combined with an incremental schedulability analysis for interacting real-time tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination language for distributed real-time systems. We implemented a logical-reliability- enhanced prototype of the compiler and runtime infrastructure for HTL. Krishnendu Chatterjee, Arkadeb Ghosal, Thomas A. Henzinger, Daniel T. Iercan, Christoph M. Kirsch, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli |
DATE | 7 |
| 2008 | Physical Architectures of Automotive SystemsabstractThis section will provide insight into new developments and advances in electronics automotive architectures. The design of innovative chip architectures, new upcoming standards for high-bandwidth and deterministic communication (FlexRay) and sensors are the domains of interest, with emphasis on reliability and support for advanced active safety functions. T. Forest, Alberto Ferrari, G. Audisio, Marco Sabatini, Alberto L. Sangiovanni-Vincentelli, Marco Di Natale |
DATE | 5 |
| 2008 | Methods, Tools and Standards for the Analysis, Evaluation and Design of Modern Automotive ArchitecturesabstractAutomotive systems are increasingly distributed and complex. Reduced time-to-market, cost and safety concerns require advance validation of the integrated systems and its components, from the functional, timing, and reliability standpoints. In particular, function correctness and performance may depend on communication and computation delays imposed by the selected architecture platform. Hence, the need for methods and tools capable of predicting the system-level timing behaviour (latencies and jitter), resulting from the HW platform selection, the synchronization between tasks and messages, and also from the synchronization and queuing policies of the middleware and RTOS levels. In this paper, we review methods and tools for the evaluation of the function performance and its timing correctness by simulation or by worst case static analysis. E. Frank, Reinhard Wilhelm, Rolf Ernst, Alberto L. Sangiovanni-Vincentelli, Marco Di Natale |
DATE | 4 |
| 2008 | Software Components for Reliable Automotive SystemsabstractSystem-level integration requires an overall understanding of the interplay of the sub-systems to enable component-based development with portability, reconfigurability and extensibility, together with guaranteed reliability and performance levels. Integration by simple interfaces and plug-and-play of sub-systems, which is the main objective of AUTOSAR, requires solving essential technical problems. We discuss to what degree the existing AUTOSAR standard can support the development of safety- and time-critical software and what is required to move toward the desirable goal of timing isolation when integrating multiple applications into the same execution platform. Harald Heinecke, Werner Damm, Bernhard Josko, Alexander Metzner, Hermann Kopetz, Alberto L. Sangiovanni-Vincentelli, Marco Di Natale |
DATE | 6 |
| 2008 | Source-Level Timing Annotation and Simulation for a Heterogeneous MultiprocessorabstractA generic and retargetable tool flow is presented that enables the export of timing data from software running on a cycle-accurate Virtual Prototype (VP) to a concurrent functional simulator. First, an annotation framework takes information gathered from running an application on the VP and automatically annotates the line-level delays back to the original source code. Then, a SystemC-based timed functional simulator runs the annotated source code much faster than the VP while preserving timing accuracy. This simulator is API-compatible with the multiprocessor's operating system. Therefore, it can compile and run unmodified applications on the host PC. This flow has been implemented for MuSIC (Multiple SIMD Cores) [6], a heterogeneous multiprocessor developed at Infineon to support Software Defined Radio (SDR). When compared with an optimized cycle-accurate VP of MuSIC on a variety of tests, including a multiprocessor JPEG encoder, the accuracy is within 20%, with speedups from 10x to 1000x. Trevor Meyerowitz, Alberto L. Sangiovanni-Vincentelli, Mirko Sauermann, Dominik Langen |
DATE | 2 |
| 2008 | Panel Session - The Future Car: Technology, Methods and ToolsabstractStart of the above-titled section of the conference proceedings record. Alberto L. Sangiovanni-Vincentelli, Marco Di Natale, Scuola S. Anna, H. Hanselmann, Harald Heinecke, Amar Bouali, Hermann Kopetz, H. Fennel, Thomas Weber 0002 |
DATE | 1 |
| 2008 | Outage-Based Rate Maximization in CDMA Wireless NetworksabstractThe problem of maximizing the sum of the transmit rates while limiting the outage probability below an appropriate threshold is investigated for networks where the nodes have limited processing capabilities. We focus on CDMA wireless network whose rates are characterized under mixed Rayleigh- lognormal fading. The outage probability is given implicitly by a complex function so that solving the optimization problem requires substantial computing. In this paper, we propose a novel explicit approximation of this function that allows solving the problem in an affordable manner. We propose two solutions of the maximization problem with the simplified outage probability constraint: one solves the problem using mixed integer-real programming. The other relaxes the constraints that rates be integers yielding a standard convex programming optimization that can be solved much faster. Numerical results show that our approaches perform well for average values of the outage requirements. Massimiliano D'Angelo, Carlo Fischione, Matteo Butussi, Alessandro Pinto, Alberto L. Sangiovanni-Vincentelli |
GLOBECOM | 5 |
| 2008 | Duty-Cycle Optimization in Unslotted 802.15.4 Wireless Sensor NetworksabstractWe present a novel approach for minimizing the energy consumption of medium access control (MAC) protocols developed for duty-cycled wireless sensor networks (WSN) for the unslotted IEEE 802.15.4 standard while guaranteeing delay and reliability constraints. The main challenge in this optimization is the random access associated with the existing IEEE 802.15.4 hardware and MAC specification that prevents controlling the exact transmission time of the packets. Data traffic, network topology, MAC, and the key parameters of duty cycles (sleep and wake time) determine the amount of random access, which in turn determines delay, reliability and energy consumption. We formulate and solve an optimization problem where the objective function is the total energy consumption in transmit, receive, listen and sleep states, subject to constraints of delay and reliability of the packet delivery and the decision variables are the sleep and wake time of the receivers. The optimal solution can be easily implemented on existing IEEE 802.15.4 hardware platforms, by storing light look-up tables in the receiver nodes. Numerical results show that the protocol outperforms significantly existing solutions. Sinem Coleri Ergen, Carlo Fischione, Dimitri Marandin, Alberto L. Sangiovanni-Vincentelli |
GLOBECOM | 4 |
| 2008 | Optimizing the Implementation of Communication in Synchronous Reactive ModelsabstractA fundamental asset of a model-based development process is the capability of providing an automatic implementation of the model that preserves its semantics and, at the same time, makes an efficient use of the resources of the execution platform. The implementation of communication between functional blocks in a synchronous reactive model requires buffering schemes and access procedures at the kernel level. Previous research has provided two competing proposals for the sizing of the communication buffer. We demonstrate how it is possible to leverage task timing information to obtain tighter bounds for the case of sporadic tasks or periodic tasks with unknown activation phase, and we propose an approach that applies to a more general model. Furthermore, we provide the description of the data structures and constant-time access procedures for writer and reader tasks, and an implementation compliant with the OSEK OS standard. Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
IEEE Real-Time and Embedded Technology and Applications Symposium | 3 |
| 2008 | Breath: A Self-Adapting Protocol for Wireless Sensor Networks in Control and AutomationabstractThe novel cross-layer protocol Breath for wireless sensor networks is designed, implemented, and experimentally evaluated. The Breath protocol is based on randomized routing, MAC and duty-cycling, which allow it to minimize the energy consumption of the network while ensuring a desired packet delivery end-to-end reliability and delay. The system model includes a set of source nodes that transmit packets via multi-hop communication to the destination. A constrained optimization problem, for which the objective function is the network energy consumption and the constraints are the packet latency and reliability, is posed and solved. It is shown that the communication layers can be jointly optimized for energy efficiency. The optimal working point of the network is achieved with a simple algorithm, which adapts to traffic variations with negligible overhead. The protocol was implemented on a test-bed with off-the-shelf wireless sensor nodes. It is compared with a standard IEEE 802.15.4 solution. Experimental results show that Breath meets the latency and reliability requirements, and that it exhibits a good distribution of the working load, thus ensuring a long lifetime of the network. Pan Gun Park, Carlo Fischione, Alvise Bonivento, Karl Henrik Johansson, Alberto L. Sangiovanni-Vincentelli |
SECON | 5 |
| 2008 | Analysis of Interference Effects in MB-OFDM UWB SystemsabstractThe inter-modulation and cross-modulation products of interferences introduced by nonlinearities of the receiver could significantly degrade system performance, and should be properly estimated when determining system design specifications. In MB-OFDM UWB systems, the traditional two- tone technique is still widely used to estimate nonlinear effects. However, this technique is not accurate enough. In this paper, we analyze the interference effects and propose a statistical approach to estimate the interference distortion products accurately. The analytical expressions for various interference scenarios are derived and then validated by simulation. Based on this analysis, we demonstrate how to adjust the two-tone technique to provide accurate distortion estimations for MB-OFDM UWB systems. Jan M. Rabaey, Alberto L. Sangiovanni-Vincentelli |
WCNC | 3 |
| 2008 | Schedulability Analysis of Petri Nets Based on Structural Properties
Cong Liu 0013, Alex Kondratyev, Yosinori Watanabe, Jörg Desel, Alberto L. Sangiovanni-Vincentelli |
Fundam. Informaticae | 5 |
| 2008 | A distributed minimum variance estimator for sensor networksabstractA distributed estimation algorithm for sensor networks is proposed. A noisy time-varying signal is jointly tracked by a network of sensor nodes, in which each node computes its estimate as a weighted sum of its own and its neighbors' measurements and estimates. The weights are adaptively updated to minimize the variance of the estimation error. Both estimation and the parameter optimization is distributed; no central coordination of the nodes is required. An upper bound of the error variance in each node is derived. This bound decreases with the number of neighboring nodes. The estimation properties of the algorithm are illustrated via computer simulations, which are intended to compare our estimator performance with distributed schemes that were proposed previously in the literature. The results of the paper allow to trading-off communication constraints, computing efforts and estimation quality for a class of distributed filtering problems. Alberto Speranzon, Carlo Fischione, Karl Henrik Johansson, Alberto L. Sangiovanni-Vincentelli |
IEEE J. Sel. Areas Commun. | 4 |
| 2008 | Implementing Synchronous Models on Loosely Time Triggered ArchitecturesabstractSynchronous systems offer a clean semantics and an easy verification path at the expense of often inefficient implementations. Capturing design specifications as synchronous models and then implementing the specifications in a less restrictive platform allow to address a much larger design space. The key issue in this approach is maintaining semantic equivalence between the synchronous model and its implementation. We address this problem by showing how to map a synchronous model onto a loosely time-triggered architecture that is fairly straightforward to implement as it does not require global synchronization or blocking communication. We show how to maintain semantic equivalence between specification and implementation using an intermediate model (similar to a Kahn process network but with finite queues) that helps in defining the transformation. Performance of the semantic preserving implementation is studied for the general case as well as for a few special cases. Stavros Tripakis, Claudio Pinello, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Paul Caspi, Marco Di Natale |
IEEE Trans. Computers | 4 |
| 2008 | Fault-Tolerant Distributed Deployment of Embedded Control SoftwareabstractSafety-critical feedback-control applications may suffer faults in the controlled plant as well as in the execution platform, i.e., the controller. Control theorists design the control laws to be robust with respect to the former kind of faults while assuming an idealized scenario for the latter. The execution platforms supporting modern real-time embedded systems, however, are distributed architectures made of heterogeneous components that may incur transient or permanent faults. Making the platform fault tolerant involves the introduction of design redundancy with obvious impact on the final cost. We present a design flow that enables the efficient exploration of redundancy/cost tradeoffs. After providing a system-level specification of the target platform and the fault model, designers can rely on the synthesis of the low-level fault-tolerance mechanisms. This is performed automatically as part of the embedded software deployment through the combination of the following three steps: replication, mapping, and scheduling. Our approach has a sound foundation in fault-tolerant data flow, a novel model of computation that simplifies the integration of formal validation techniques. Finally, we report on the application of our design flow to two case studies from the automotive industry: a steer-by-wire system from General Motors and a drive-by-wire system from BMW. Claudio Pinello, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2008 | An FSM Reengineering Approach to Sequential Circuit Synthesis by State SplittingabstractThis paper presents a finite-state machine (FSM) reengineering method that enhances the FSM synthesis by reconstructing a functionally equivalent but topologically different FSM based on the optimization objective. This method enables the FSM synthesis algorithms to explore a set of functionally equivalent FSMs and obtain better solutions than those in the original FSM. To demonstrate the effectiveness of the proposed method, we apply it to popular power- and area-driven FSM synthesis algorithms, respectively. Our method achieves an average of 5.5% power reduction and 2.7% area reduction, respectively, on 25 Microelectronics Center of North Carolina (MCNC) FSM benchmarks, where the proposed method is applicable. This is a significant performance improvement for the power- and area-driven FSM synthesis algorithms being used. Our method has a negligible run-time overhead, and it maintains the quality of the synthesis solutions. Gang Qu 0001, Tiziano Villa, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 2008 | Composing heterogeneous reactive systemsabstractWe present a compositional theory of heterogeneous reactive systems. The approach is based on the concept of tags marking the events of the signals of a system. Tags can be used for multiple purposes from indexing evolution in time (time stamping) to expressing relations among signals, like coordination (e.g., synchrony and asynchrony) and causal dependencies. The theory provides flexibility in system modeling because it can be used both as a unifying mathematical framework to relate heterogeneous models of computations and as a formal vehicle to implement complex systems by combining heterogeneous components. In particular, we introduce an algebra of tag structures to define heterogeneous parallel composition formally. Morphisms between tag structures are used to define relationships between heterogeneous models at different levels of abstraction. In particular, they can be used to represent design transformations from tightly synchronized specifications to loosely-synchronized implementations. The theory has an important application in the correct-by-construction deployment of synchronous design on distributed architectures. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Embed. Comput. Syst. | 5 |
| 2007 | Period Optimization for Hard Real-time Distributed Automotive SystemsabstractThe complexity and physical distribution of modern active-safety automotive applications requires the use of distributed architectures. These architectures consist of multiple electronic control units (ECUs) connected with standardized buses. The most common configuration features periodic activation of tasks and messages coupled with run-time priority-based scheduling. The correct deployment of applications on such architectures requires end-to-end latency deadlines to be met. This is challenging since deadlines must be enforced across a set of ECUs and buses, each of which supports multiple functionality. The need for accommodating legacy tasks and messages further complicates the scenario. Abhijit Davare, Qi Zhu 0002, Marco Di Natale, Claudio Pinello, Sri Kanajan, Alberto L. Sangiovanni-Vincentelli |
DAC | 6 |
| 2007 | Electronics: The New Differential in the Automotive Industry
Nick Smith, Andrew Chien, Christopher Hegarty, Walden C. Rhines, Alberto L. Sangiovanni-Vincentelli, Frank Winters |
DAC | 5 |
| 2007 | Synthesis of task and message activation models in real-time distributed automotive systemsabstractModern automotive architectures support the execution of distributed safety- and time-critical functions on a complex networked system with several buses and tens of ECUs. Schedulability theory allows the analysis of the worst case end-to-end latencies and the evaluation of the possible architecture configurations options with respect to timing constraints. The paper presents an optimization framework, based on an ILP formulation of the problem, to select the communication and synchronization model that leverages the trade-offs between the purely periodic and the precedence constrained data-driven activation models to meet the latency and jitter requirements of the application. The authors demonstrate its effectiveness by optimizing a complex automotive architecture Marco Di Natale, Claudio Pinello, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli |
DATE | 5 |
| 2007 | Loosely time-triggered architectures based on communication-by-samplingabstractWe address the problem of mapping a set of processes which communicate synchronously on a distributed platform. The Time Triggered Architecture (TTA) proposed by Kopetz for the communication mechanism of a distributed platform offers a direct mapping that would preserve the semantics of the specification. However, its exact implementation may, at times, be problematic as it requires the distributed platform to have the clocks of its components perfectly synchronized. We propose as implementation architecture a relaxation of TTA called Loosely Time-Triggered Architecture (LTTA), in which computing units perform writes into and reads from the communication medium independently, triggered by local, quasi-periodic but non synchronized, clocks. LTTA offers some of the advantages of TTA with lower hardware cost and greater flexibility. So far LTTA was studied for single directional two-users communications over an LTT bus. General topology was not studied. In this paper we propose a design flow that ensures semantics preservation for an LTT communication network with arbitrary topology. Key elements are two new protocols for clock regeneration and predictive traffic shaping. Our approach relies on a mathematical Model of Communication (MoC) that we describe in detail. Albert Benveniste, Paul Caspi, Marco Di Natale, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis |
EMSOFT | 5 |
| 2007 | A communication synthesis infrastructure for heterogeneous networked control systems and its application to building automation and controlabstractIn networked control systems the controller of a physically-distributed plant is implemented as a collection of tightly-interacting, concurrent processes running on a distributed execution platform. The execution platform consists of a set of heterogeneous components (sensors, actuators, and controllers) that interact through a hierarchical communication network. We propose a methodology and a framework for design exploration and automatic synthesis of the communication network. We present how our approach can be applied to the design of control systems for intelligent buildings. The input specification of the control system includes (i) the constraints on the location of its components, which are imposed by the plant, (ii) the communication requirements among the components, and (iii) an estimation of the real-time constraints for the correct behavior of the algorithms implementing the control law. The output produces an implementation of the control networks that is obtained by combining elements from a pre-defined library of communication links, protocols, interfaces, and switches. The implementation is optimal in the sense that it satisfies the given specification while minimizing an objective function that captures the overall cost of the network implementation. Alessandro Pinto, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 3 |
| 2007 | A new algorithm for the largest compositionally progressive solution of synchronous language equationsabstractThe paper addresses the problem of designing a component that combined with a known part of a system, called the context FSM, is a reduction of a given specification FSM. We study compositionally progressive solutions of synchronous FSM equations. Such solutions, when combined with the context, do not block any input that may occur in the specification, so they are of practical use. We show that if a synchronous FSM equation has a compositionally progressive solution, then the equation has the largest compositionally progressive solution. We provide an algorithm to compute the largest compositionally progressive solution that splits states of the largest solution and then removes those inducing a non-progressive composition. Tiziano Villa, Svetlana Zharikova, Nina Yevtushenko 0001, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ACM Great Lakes Symposium on VLSI | 5 |
| 2007 | Optimizing End-to-End Latencies by Adaptation of the Activation Events in Distributed Automotive SystemsabstractSchedulability theory provides support for the analysis of the worst case latencies in distributed computations when the architecture of the system is known and the communication and synchronization mechanisms have been defined. In the design of complex automotive systems, however, a great benefit of schedulability analysis may come from its use as an aid in the exploration of the software architecture configurations that can best support the target application. We present an optimization algorithm that leverages the trade-offs between the purely periodic and the data-driven activation models to meet the latency requirements of distributed vehicle functions. We demonstrate its effectiveness on a complex automotive architecture Marco Di Natale, Claudio Pinello, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli |
IEEE Real-Time and Embedded Technology and Applications Symposium | 5 |
| 2007 | Definition of Task Allocation and Priority Assignment in Hard Real-Time Distributed SystemsabstractThe complexity and physical distribution of modern active safety, chassis and powertrain automotive applications requires the use of distributed architectures. Complex functions designed as networks of function blocks exchanging signal information are deployed onto the physical HW and implemented in a SW architecture consisting of a set of tasks and messages. The typical configuration features priority-based scheduling of tasks and messages and imposes end- to-end deadlines. In this work, we optimize the task placement and the signal to message mapping and we automate the assignment of priorities to tasks and messages in order to meet end-to-end deadline constraints and minimize latencies. This is accomplished by leveraging worst case response time analysis within a mixed integer linear optimization framework. Our approach is applied to an automotive case study to prove its feasibility. Qi Zhu 0002, Marco Di Natale, Alberto L. Sangiovanni-Vincentelli |
RTSS | 4 |
| 2007 | E2RINA: an Energy Efficient and Reliable In-Network Aggregation for Clustered Wireless Sensor NetworksabstractThe paper presents E2RINA, an aggregation algorithm for wireless sensor network applications characterized by clustered topologies, such as building automation and manufacturing plants. Thank to an efficient use of the wireless channel, E2RINA offers the robustness of the gossip-based algorithms and, at the same time, the energy performance of the faster cluster head-based algorithms. A mathematical model to predict the performance of the algorithm with respect to the free variables without the need of extensive simulations was also developed. The model was validated and the robustness of E2RINA by running a simulation model of a test case consisting of a cluster of MICA nodes. Luca Necchi, Alvise Bonivento, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli, Laura Vanzago |
WCNC | 4 |
| 2007 | Refinement preserving approximations for the design and verification of heterogeneous systems
Roberto Passerone, Jerry R. Burch, Alberto L. Sangiovanni-Vincentelli |
Formal Methods Syst. Des. | 3 |
| 2007 | Quo Vadis, SLD? Reasoning About the Trends and Challenges of System Level DesignabstractSystem-level design (SLD) is considered by many as the next frontier in electronic design automation (EDA). SLD means many things to different people since there is no wide agreement on a definition of the term. Academia, designers, and EDA experts have taken different avenues to attack the problem, for the most part springing from the basis of traditional EDA and trying to raise the level of abstraction at which integrated circuit designs are captured, analyzed, and synthesized from. However, my opinion is that this is just the tip of the iceberg of a much bigger problem that is common to all system industry. In particular, I believe that notwithstanding the obvious differences in the vertical industrial segments (for example, consumer, automotive, computing, and communication), there is a common underlying basis that can be explored. This basis may yield a novel EDA industry and even a novel engineering field that could bring substantial productivity gains not only to the semiconductor industry but to all system industries including industrial and automotive, communication and computing, avionics and building automation, space and agriculture, and health and security, in short, a real technical renaissance. In this paper, I present the challenges faced by industry in system level design. Then, I propose a design methodology, platform-based design (PBD), that has the potential of addressing these challenges in a unified way. Further, I place methodology and tools available today in the PBD framework and present a tool environment, Metropolis, that supports PBD and that can be used to integrate available tools and methods together with two examples of its application to separate industrial domains Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 1 |
| 2007 | Remembering Richard [Obituary, Richard A.Newton]abstractRecounts the life and career of A. Richard Newton and provides an excerpt of his keynote address at the 1995 Design Automation Conference and an unabridged presentation of his address to the Berkeley EECS Annual Research Symposium on February 23, 2006. Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 2007 | Techniques for maintaining connectivity in wireless ad-hoc networks under energy constraintsabstractDistributed wireless systems (DWSs) are emerging as the enabler for next-generation wireless applications. There is a consensus that DWS-based applications, such as pervasive computing, sensor networks, wireless information networks, and speech and data communication networks, will form the backbone of the next technological revolution. Simultaneously, with great economic, industrial, consumer, and scientific potential, DWSs pose numerous technical challenges. Among them, two are widely considered as crucial: autonomous localized operation and minimization of energy consumption. We address the fundamental problem of how to maximize the lifetime of the network using only local information, while preserving network connectivity. We start by introducing the care-free sleep (CS) Theorem that provides provably optimal conditions for a node to go into sleep mode while ensuring that global connectivity is not affected. The CS theorem is the basis for an efficient localized algorithm that decides which nodes will go to into sleep mode and for how long. We have also developed mechanisms for collecting neighborhood information and for the coordination of distributed energy minimization protocols. The effectiveness of the approach is demonstrated using a comprehensive study of the performance of the algorithm over a wide range of network parameters. Another important highlight is the first mathematical and Monte Carlo analysis that establishes the importance of considering nodes within a small number of hops in order to preserve energy. Farinaz Koushanfar, Abhijit Davare, David T. Nguyen, Alberto L. Sangiovanni-Vincentelli, Miodrag Potkonjak |
ACM Trans. Embed. Comput. Syst. | 4 |
| 2007 | Uniprocessor scheduling under precedence constraints for embedded systems designabstractIn this paper, we present a novel approach to the constrained scheduling problem, while addressing a more general class of constraints that arise from the timing requirements on real-time embedded controllers. We provide general necessary and sufficient conditions for scheduling under precedence constraints and derive sufficient conditions for two well-known scheduling policies. We define mathematical problems that provide optimum priority and deadline assignments, while ensuring both precedence constraints and system's schedulability. We show how these problems can be relaxed to corresponding integer linear programming (ILP) formulations leveraging on available solvers. The results are demonstrated on a real design case. Leonardo Mangeruca, Massimo Baleani, Alberto Ferrari, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Embed. Comput. Syst. | 4 |
| 2007 | System Level Design for Clustered Wireless Sensor NetworksabstractWe present a system level design methodology for clustered wireless sensor networks based on a semi-random communication protocol called SERAN, a mathematical model that allows to optimize the protocol parameters, and a network initialization and maintenance procedure. SERAN is a two-layer (routing and MAC) protocol. At both layers, SERAN combines a randomized and a deterministic approach. While the randomized component provides robustness over unreliable channels, the deterministic component avoids an explosion of packet collisions and allows our protocol to scale with network size. The combined result is a high reliability and major energy savings when dense clusters are used. Our solution is based on a mathematical model that characterizes performance accurately without resorting to extensive simulations. Thanks to this model, the user needs only to specify the application requirements in terms of end-to-end packet delay and packet loss probability, select the intended hardware platform, and the protocol parameters are set automatically to satisfy latency requirements and optimize for energy consumption. Alvise Bonivento, Carlo Fischione, Luca Necchi, Fernando Pianegiani, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Ind. Informatics | 5 |
| 2007 | Semantics-Preserving Design of Embedded Control Software from Synchronous ModelsabstractThe design of embedded controllers is experiencing a growth in complexity as embedded systems increase their functionality while they become ubiquitous in electronic appliances, cars, airplanes, etc. As requirements become more challenging, mathematical models gain importance for mastering complexity. Among the different computational models proposed, synchronous models have proved to be the most widely used for control dominated applications. While synchronous models simplify the way of dealing with concurrency by decoupling functional and timing aspects, their software implementation on multitasking and multiprocessor platforms is far from straightforward, because of the asynchronous nature of most industrial software platforms. Known solutions in the literature either restrict the solution space or focus on special cases. We present a method for preserving the synchronous semantics through buffer-based intertask communication mechanisms, grounded on an abstraction of the target platform. This allows us to deal with any task set and, most importantly, being independent of the implementation, to explore the design space effectively. Leonardo Mangeruca, Massimo Baleani, Alberto Ferrari, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Software Eng. | 4 |
| 2006 | Automotive electronics: steady growth for years to come!abstractThe world of electronics is witnessing a revolution in the way products are conceived, designed and implemented. The ever growing importance of the web, the advent of microprocessors of great computational power, the explosion of wireless communication, the development of new generations of integrated sensors and actuators are changing the world in which we live and work. The new key words are:• Disappearing electronics, i.e., electronics has to be invisible to the user, it has to help unobtrusively.• Pervasive computing, i.e., electronics is everywhere, all common use objects will have an electronic dimension.• Ambient intelligence, i.e., the environment will react to us with the use of electronic components. They will recognize who we are and what we like.• Wearable computing, i.e., the new devices will be worn as a watch or a hat. They will become part of our clothes. Some of these devices will be tags that will contain all important information about us.• Know more, carry less, i.e., the environment will know more about us so that we will not need to carry all the paraphernalia of keys, credit cards, personal I.D.s, access cards, access codes. Alberto L. Sangiovanni-Vincentelli |
ASP-DAC | 1 |
| 2006 | Randomized protocol stack for ubiquitous networks in indoor environmentabstractAbstract — We present a novel protocol architecture for ubiquitous networks. Our solution is based on a randomized routing, MAC and duty cycling protocols that allow for performance and reliability leveraging node density. We show how the three layers can be jointly optimized for energy efficiency and we present a completely distributed algorithm that allows for the network to reach the optimal working point and adapt to traffic variations with negligible overhead. Finally, we present a set of simulation results that support our mathematical model. I. Alvise Bonivento, Carlo Fischione, Alberto L. Sangiovanni-Vincentelli |
CCNC | 3 |
| 2006 | Performance analysis of collaborative spatio-temporal processing for wireless sensor networksabstractAbstract — Spatio-Temporal processing is a control technique to increase the quality of the received signals in wireless networks. Outage events have a strong influence not only on the performance of the physical layer, but also on routing, MAC, and application layer. In this paper, we propose an outage based performance analysis of collaborative STP for WSNs. After an accurate characterization of the wireless channel, we derive the outage statistics as function of the STP coefficients, and investigate the effects of STP on the probability, average duration and rate of the outage events. Furthermore, we show that a proper control policy of the STP coefficients can be derived according to the requirements from the applications and WSNs communication layers. Carlo Fischione, Alvise Bonivento, Alberto L. Sangiovanni-Vincentelli, Fortunato Santucci, Karl Henrik Johansson |
CCNC | 3 |
| 2006 | SAT sweeping with local observability don't-caresabstractSAT sweeping is a method for simplifying an shape And/Inverter graph (AIG) by systematically merging graph vertices from the inputs towards the outputs using a combination of structural hashing, simulation, and SAT queries. Due to its robustness and efficiency, SAT sweeping provides a solid algorithm for Booleanreasoning in functional verification and logic synthesis. In previous work, SAT sweeping merges two vertices only if they are functionally equivalent. In this paper we present a significant extension of the SAT-sweeping algorithm that exploits local observability don't-cares (ODCs) to increase the number of vertices merged. We use a novel technique to bound the use of ODCs and thus the computational effort to find them, while still finding a large fraction of them. Our reported results based on a set of industrial benchmark circuits demonstrate that ODC-based SAT sweeping results in significantly more graph simplification with great benefit for Boolean reasoning with a moderate increase in computational effort. Qi Zhu 0002, Nathan Kitchen, Andreas Kuehlmann, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 2006 | Platform-based design of wireless sensor networks for industrial applicationsabstractWe present a methodology, an environment and supporting tools to map an application on a wireless sensor network (WSN). While the method is quite general, we use extensively an example in the domain of industrial control as it is one of the most promising application of WSN and yet it is largely untouched by it. Our design flow starts from a high level description of the control algorithm and a set of candidate hardware platforms and automatically derives an implementation that satisfies system requirements while optimizing for power consumption. To manage the heterogeneity and complexity inherent in this rather complete design flow, we identify three abstraction layers and introduce the tools to transition between different layers and obtain the final solution. We present a case study of a control application for manufacturing plants that shows how the methodology covers all the aspects of the design process, from conceptual description to implementation Alvise Bonivento, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
DATE | 3 |
| 2006 | FPGA architecture characterization for system level performance analysisabstractWe present a modular and scalable approach for automatically extracting actual performance information from a set of FPGA-based architecture topologies. This information is used dynamically during simulation to support performance analysis in a system level design environment. The topologies capture systems representing common designs using FPGA technologies of interest. Their characterization is done only once; the results are then used during simulation of actual systems being explored by the designer. Our approach allows a rich set of FPGA architectures to be explored accurately at various abstraction levels to seek optimized solutions with minimal effort by the designer. To offer an industrial example of our results, we describe the characterization process for Xilinx Core Connect-based platforms and the integration of this data into the METROPOLIS modeling environment Douglas Densmore, Adam Donlin, Alberto L. Sangiovanni-Vincentelli |
DATE | 3 |
| 2006 | Exploring trade-off's between centralized versus decentralized automotive architectures using a virtual integration environmentabstractThe large variety of architectural dimensions in automotive electronics design, for example, bus protocols, number of nodes, sensors and actuators interconnections and power distribution topologies, makes architecture design task a very complex but crucial design step especially for OEMs. This situation motivates the need for a design environment that accommodates the integration of a variety of models in a manner that enables the exploration of design alternatives in an efficient and seamless fashion. Exploring these design alternatives in a virtual environment and evaluating them with respect to metrics such as cost, latency, flexibility and reliability provide an important competitive advantage to OEMs and help minimize integration risks later in the design cycle. In particular, the choice of the degree of decentralization of the architecture has become a crucial issue in automotive electronics. In this paper, we demonstrate how a rigorous methodology (platform-based design) and the Metropolis framework can be used to find the balance between centralized and decentralized architectures Sri Kanajan, Haibo Zeng 0001, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli |
DATE | 4 |
| 2006 | Is "Network" the next "Big Idea" in design?abstractAs the complexity of nowadays systems continues to grow, we are moving away from creating individual components from scratch, toward methodologies that emphasize composition of re-usable components via the network paradigm. Complex component interactions can create a range of amazing behaviors, some useful, some unwanted, some even dangerous. To manage them, a "science" for network design is evolving, applicable in some surprising areas. In this paper, we consider a few application domains and discus the design challenges involved from a methodology standpoint. From large-scale hardware/software systems, to dynamically adaptive sensor networks, and network-on-chip architectures, these ideas find wide application Radu Marculescu, Jan M. Rabaey, Alberto L. Sangiovanni-Vincentelli |
DATE | 3 |
| 2006 | Communication and co-simulation infrastructure for heterogeneous system integrationabstractWith the increasing complexity and heterogeneity of embedded electronic systems, a unified design methodology at higher levels of abstraction becomes a necessity. Meanwhile, it is also important to incorporate the current design practice emphasizing IP reuse at various abstraction levels. However, the abstraction gap prohibits easy communication and synchronization in IP integration and co-simulation. In this paper, we present a communication infrastructure for an integrated design framework that enables co-design and co-simulation of heterogeneous design components specified at different abstraction levels and in different languages. The core of the approach is to abstract different communication interfaces or protocols to a common high level communication semantics. Designers only need to specify the interfaces of the design components using extended regular expressions; communication adapters can then be automatically generated for the co-simulation or other co-design and co-verification purposes. Guang Yang 0004, Xi Chen 0024, Felice Balarin, Harry Hsieh, Alberto L. Sangiovanni-Vincentelli |
DATE | 5 |
| 2006 | Communication by sampling in time-sensitive distributed systemsabstractIn time-sensitive systems writing to and reading from the communication medium is on a purely time-triggered but asynchronous basis. Writes and reads can occur at any time and the data are stored and sustained until overwritten. We study how to maintain data semantics when the duration of the actions change from specification to implementation.In doing so, we rely on tag systems formerly introduced by the authors. The exibility of tag systems allows handling the problem in a formal, yet tractable way. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis |
EMSOFT | 5 |
| 2006 | A hierarchical coordination language for interacting real-time tasksabstractWe designed and implemented a new programming language called Hierarchical Timing Language (HTL) for hard realtime systems. Critical timing constraints are specified within the language,and ensured by the compiler. Programs in HTL are extensible in two dimensions without changing their timing behavior: new program modules can be added, and individual program tasks can be refined. The mechanism supporting time invariance under parallel composition is that different program modules communicate at specified instances of time. Time invariance under refinement is achieved by conservative scheduling of the top level. HTL is a coordination language, in that individual tasks can be implemented in "foreign" languages. As a case study, we present a distributed HTL implementation of an automotive steer-by-wire controller. Arkadeb Ghosal, Alberto L. Sangiovanni-Vincentelli, Christoph M. Kirsch, Thomas A. Henzinger, Daniel T. Iercan |
EMSOFT | 2 |
| 2006 | Robust system level design with analog platformsabstractAn approach to robust system level mixed signal design is presented based on analog platforms. The bottom-up characterization phase of platform components provides accurate performance models that export architectural constraints to the system level. From the one side, performance models can be affected by residual errors and usually do not consider process variations and modeling uncertainties. Conversely, behavioral models cannot match accurate circuit level simulations, so that during the mapping (exploration) process circuit configurations difficult to be realized may be obtained. We propose a methodology that extends techniques from optimization and design centering to system level analog design exploiting general, implicit architectural constraints to control the robustness of the solution. The approach allows quantitative extension of robust techniques to hierarchical designs. Its effectiveness is illustrated with the design of a pipeline A/D converter and a UMTS receiver front-end. Fernando De Bernardinis, Pierluigi Nuzzo 0001, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 2006 | Yield prediction for 3D capacitive interconnectionsabstractCapacitive interconnections are very promising structures for high-speed and low-power signaling in 3D packages. Since the performance of AC links, in terms of Band-Width and Bit-Error-Rate (BER), depends on assembly and synchronization accuracy we performed a statistical analysis of assembly procedures and communication circuits. In this paper we present a yield prediction methodology for 3D capacitive links: starting from the analysis of communication circuits and BER measurements, we analyze stacking variability in order to predict reliability and performance. The proposed parametric yield analysis is demonstrated on a test-case, with constrained inter-electrode coupling and operating frequency. Alberto Fazzi, Luca Magagni, Mario de Dominicis, Paolo Zoffoli, Roberto Canegallo, Pier Luigi Rolandi, Alberto L. Sangiovanni-Vincentelli, Roberto Guerrieri |
ICCAD | 7 |
| 2006 | A semantic-driven synthesis flow for platform-based designabstractIn this work, we propose a semantics-driven synthesis flow, in which the semantics and the abstraction level are determined formally by using the concept of a common modeling domain between functionality and architecture. By doing so, a formal synthesis procedure can be defined and algorithms for automatic optimal mapping derived. Qi Zhu 0002, Abhijit Davare, Alberto L. Sangiovanni-Vincentelli |
MEMOCODE | 3 |
| 2006 | Modeling and Early Performance Estimation for Network Processor Applications
Antonia Bertolino, Alvise Bonivento, Guglielmo De Angelis, Alberto L. Sangiovanni-Vincentelli |
MoDELS | 4 |
| 2006 | Cooperative Diversity with Disconnection Constraints and Sleep Discipline for Power Control in Wireless Sensor NetworksabstractWe derive a power control policy for a group of sensor nodes that are monitoring a real-time application sensitive to disconnections (outages) of the communication. Specifically, we suggest that the sensor nodes perform cooperative diversity while running a sleep discipline. After the description of a detailed model of the wireless links, we propose a power minimization algorithm with a constraint expressed in terms of outage probability. Suboptimal solutions are also discussed. Numerical examples are provided for various number of nodes, wireless scenarios and nodes activities. It is argued that nodes with reduced activity show better performance Carlo Fischione, Alvise Bonivento, Karl Henrik Johansson, Alberto L. Sangiovanni-Vincentelli |
VTC Spring | 4 |
| 2006 | A Framework for Modeling the Distributed Deployment of Synchronous Designs
Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
Formal Methods Syst. Des. | 2 |
| 2006 | Platform based design for wireless sensor networks
Alvise Bonivento, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
Mob. Networks Appl. | 3 |
| 2006 | L. Embedding Mixed-Signal Design in Systems-on-ChipabstractWith semiconductor technology feature size scaling below 100 nm, mixed-signal design faces some important challenges, caused among others by reduced supply voltages, process variation, and declining intrinsic device gains. Addressing these challenges requires innovative solutions, at the technology, circuit, architecture, and design-methodology level. We present some of these solutions, including a structured platform-based design methodology to enable a meaningful exploration of the broad design space and to classify potential solutions in terms of the relevant metrics. Jan M. Rabaey, Fernando De Bernardinis, Ali M. Niknejad, Borivoje Nikolic, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 5 |
| 2006 | Complexity of two-level logic minimizationabstractThe complexity of two-level logic minimization is a topic of interest to both computer-aided design (CAD) specialists and computer science theoreticians. In the logic synthesis community, two-level logic minimization forms the foundation for more complex optimization procedures that have significant real-world impact. At the same time, the computational complexity of two-level logic minimization has posed challenges since the beginning of the field in the 1960s; indeed, some central questions have been resolved only within the last few years, and others remain open. This recent activity has classified some logic optimization problems of high practical relevance, such as finding the minimal sum-of-products (SOP) form and maximal term expansion and reduction. This paper surveys progress in the field with self-contained expositions of fundamental early results, an account of the recent advances, and some new classifications. It includes an introduction to the relevant concepts and terminology from computational complexity, as well a discussion of the major remaining open problems in the complexity of logic minimization Christopher Umans, Tiziano Villa, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2006 | System level design paradigms: Platform-based design and communication synthesisabstractEmbedded system level design must be based on paradigms that make formal foundations and unification a cornerstone of their construction. Platform-Based designs and communication synthesis are important components of the paradigm shift we advocate.Communication synthesis is a fundamental productivity tool in a design methodology where reuse is enforced. Communication design in a reuse methodology starts with a set of functional requirements and constraints on the interaction among components and then proceeds to build protocols, topology, and physical implementations that satisfy requirements and constraints while optimizing appropriate measures of efficiency of the implementation. Maximum efficiency can be reached when the communication specifications are entered at high levels of abstraction and the design process optimizes the implementation from this specification. Unfortunately, this process is very difficult if it is not cast in a rigorous framework. Platform-Based design helps define a successive refinement process where each step can be carried out automatically and optimized appropriately. We present two cases, an on-chip and a wireless sensor network design, where the resulting methodology gave encouraging results. Alessandro Pinto, Alvise Bonivento, Alberto L. Sangiovanni-Vincentelli, Roberto Passerone, Marco Sgroi |
ACM Trans. Design Autom. Electr. Syst. | 3 |
| 2005 | FSM re-engineering and its application in low power state encodingabstractWe propose Finite State Machine (FSM) re-engineering, a performance enhancement framework for FSM synthesis and optimization procedure. We start with any traditional FSM synthesis and optimization procedure; then re-construct a functionally equivalent but topologically different FSM based on the optimization objective; and conclude with another round of FSM synthesis and optimization (can be the same procedure) on the newly constructed FSM. This allows us to explore a larger solution space that includes synthesis solutions to the functionally equivalent FSMs instead of only the original FSM, making it possible to obtain solutions better than the optimal ones for the original FSM. Guided by the result of the first round FSM synthesis, the solution space exploration process can be rapid and cost-efficient.To demonstrate this framework, we develop a genetic algorithm and a fast heuristic to re-engineer a low power state encoding procedure POW3 [1]. On average, POW3 can reduce the switching activity by 12% over non-power-driven state encoding schemes on the MCNC FSM benchmarks. We then re-engineer these benchmarks by the proposed genetic algorithm and heuristic respectively. When we apply POW3 to the re-engineered FSMs, we observe an additional 8.9% and 6.0% switching activity reduction. This translates to an average of 7.9% energy reduction with little area increase. Finally, we obtain the optimal low power coding for benchmarks of small size from an integer linear programming formulation. We find that the POW3-encoded original FSMs are 27.0% worse than the optimal, but this number drops to 6.7% when we apply POW3 to the re-engineered FSMs. Gang Qu 0001, Tiziano Villa, Alberto L. Sangiovanni-Vincentelli |
ASP-DAC | 4 |
| 2005 | Mixed signal design space exploration through analog platformsabstractWe propose a hierarchical mixed signal design methodology based on the principles of Platform-Based Design (PBD). The methodology is a meet-in-the-middle approach where design components are modeled bottom-up at various abstraction levels and performance constraints are mapped top-down to select among the available components the ones that best meet the constraints. The design methodology can seamlessly operate on both analog and digital designs, thus dealing with mixed signal designs in a consistent way. We demonstrate the effectiveness of the approach optimizing an 80 MS/s 14 bit pipelined Analog-to-Digital Converter (ADC) including digital calibration, yielding 64% power reduction compared to the original hand optimized design. Fernando De Bernardinis, Pierluigi Nuzzo 0001, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 2005 | Simulation based deadlock analysis for system level designsabstractIn the design of highly complex, heterogeneous, and concurrent systems, deadlock detection and resolution remains an important issue. In this paper, we systematically analyze the synchronization dependencies in concurrent systems modeled in the Metropolis design environment, where system functions, high level architectures and function-architecture mappings can be modeled and simulated. We propose a data structure called the dynamic synchronization dependency graph, which captures the runtime (blocking) dependencies. A loop-detection algorithm is then used to detect deadlocks and help designers quickly isolate and identify modeling errors that cause the deadlock problems. We demonstrate our approach through a real world design example, which is a complex functional model for video processing and a high level model of function-architecture mapping. Xi Chen 0024, Abhijit Davare, Harry Hsieh, Alberto L. Sangiovanni-Vincentelli, Yosinori Watanabe |
DAC | 4 |
| 2005 | Correct-by-Construction Transformations across Design Environments for Model-Based Embedded Software DevelopmentabstractEmbedded software design for real time reactive systems has become the bottleneck in their market introduction into complex products such as automobiles, airplanes, and industrial control plant. In particular, functional correctness and reactive performance are increasingly difficult to verify. The advent of model-based design methodologies has alleviated some of the verification-related problems by making the code-generation process flow automatically from the model description. Given the relative infancy of this approach, several companies rely upon design flows based on different tools connected together by file transfer. This way of integrating tools defeats the very purpose of the methodology, introducing a high potential of errors in the transformation from one format to another and preventing formal analysis of the properties of the design. We propose to adopt a formal transformation across different tools and we give an example of this approach by linking two tools that are widely used in the automotive domain, Simulink and ASCET. We believe that this approach can be applied to any embedded software design flow to leverage the power of all the tools in the flow. Massimo Baleani, Alberto Ferrari, Leonardo Mangeruca, Alberto L. Sangiovanni-Vincentelli, Ulrich Freund, Erhard Schlenker, Hans-Jörg Wolff |
DATE | 4 |
| 2005 | Integrated Electronics in the Car and the Design Chain Evolution or Revolution?abstractTo deliver better-performing, less-expensive, and safer cars with increasingly tighter time-to-market constraints imposed by worldwide competitiveness, the future development process for automotive electronic systems must provide solutions to: the design of complex functionality with tight requirements on safety and correctness; the design of distributed architectures consisting of several subsystems with constraints on nonfunctional metrics such as cost, power consumption, weight, position, and reliability; and the mapping of the functionality (often implemented as OEM application software) onto the components of a distributed architecture with tight real-time and communication constraints. Alberto L. Sangiovanni-Vincentelli |
DATE | 1 |
| 2005 | Efficient embedded software design with synchronous modelsabstractModel-based design is an important approach for embedded software. The method starts from a mathematical representation of the design problem and derives the software implementation from this representation. The model that has had most success especially for control dominated application is synchronous reactive. While this model simplifies the way of dealing with concurrency by decoupling functional and timing aspects, when implemented, it may be inefficient since the synchronous assumption implies constraints that are stronger than needed. We present in this paper a method for improving the efficiency of the software design process, by relaxing computation constraints, while preserving the synchronous computation semantics, with the introduction of a particular inter-task communication mechanism. We show how this mechanism can be implemented on single processor, multi processor and distributed implementation platforms. Massimo Baleani, Alberto Ferrari, Leonardo Mangeruca, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 4 |
| 2005 | Tag machinesabstractHeterogeneity is a challenge to overcome in the design of embedded systems. We presented in the recent past a theory for the composition of heterogeneous components based on tagged systems, a behavioral (denotational) framework. in this paper, we present an operational view of tagged systems, where we focus on tag machines as mathematical artifacts that act as finitary generators of tagged systems. Properties of tag machines are investigated. A fundamental theorem on homogeneous compositionality is given as a first step towards an operational theory of heterogeneous systems. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 4 |
| 2005 | Rialto: a bridge between description and implementation of control algorithms for wireless sensor networksabstractRialto is a design framework that allows separating the description of a control application for wireless sensor networks from its physical network implementation. The methodology supported by Rialto consists of two steps: Alvise Bonivento, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 3 |
| 2005 | A structural approach to quasi-static schedulability analysis of communicating concurrent programsabstractWe describe a system as a set of communicating concurrent programs. Quasi-static scheduling compiles the concurrent programs into a sequential one. It uses a Petri net as an intermediate model of the system. However, Petri nets generated from many interesting applications are not schedulable. In this paper, we show the underlying mechanism which causes unschedulability in terms of the structure of a Petri net. We introduce a Petri net structural property and prove unschedulability if the property holds. We propose a linear programming based algorithm to check the property, and prove the algorithm is valid. Our approach prove unschedulability typically within a second for Petri nets generated from industrial JPEG and MPEG codecs, while the scheduler fails to terminate within 24 hours. Cong Liu 0013, Alex Kondratyev, Yosinori Watanabe, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 4 |
| 2005 | A formal approach to fault tree synthesis for the analysis of distributed fault tolerant systemsabstractDesigning cost-sensitive real-time control systems for safety-critical applications requires a careful analysis of both performance versus cost aspects and fault coverage of fault tolerant solutions. This further complicates the difficult task of deploying the embedded software that implements the control algorithms on a possibly distributed execution platform (for instance in automotive applications). In this paper, we present a novel technique for constructing a fault tree that models how component faults may lead to system failure. The fault tree enables us to use existing commercial analysis tools to assess a number of dependability metrics of the system. Our approach is centered on a model of computation, Fault Tolerant Data Flow (FTDF), that enables the integration of formal verification techniques. This new analysis capability is added to an existing design framework, also based on FTDF, that enables a synthesis-based, correct-by-construction, design methodology for the deployment of real-time feedback control systems in safety critical applications. Mark L. McKelvin Jr., Gabriel Eirea, Claudio Pinello, Sri Kanajan, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 5 |
| 2005 | Efficient analog platform characterization through analog constraint graphsabstractWe propose a scheme for improving the efficiency of the characterization process for system-level models of analog circuits within the analog platform based design paradigm. We leverage designer knowledge to map basic functional requirements of the circuit into circuit parameters relations so that the sampling space can be significantly reduced. A set of equalities and inequalities in the circuit parameters is used to represent the constraints. A feasible parameter space lies at the intersection of the sets of design parameters that satisfy equalities and inequalities, defining a manifold in the parameter space. We introduce a bipartite graph representation denoted analog constraint graphs (ACG) to represent these constraints. ACGs are instrumental for obtaining a random configuration generator that samples configurations in the manifold. The sampler is automatically translated into executable code to fit the characterization framework starting from a mathematical description of constraints. Results show that the automatically generated samplers are comparable in terms of code efficiency with hand-written ones. Furthermore, a heuristics to generate uniformly distributed configuration enabled by the tools is presented and applied to a complex ADC design, yielding a reduction in power consumption by more than 28%. Fernando De Bernardinis, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 2005 | SERAN: a semi random protocol solution for clustered wireless sensor networksabstractSERAN is a two-layer (routing and MAC) protocol for wireless sensor networks in manufacturing plants. At both layers, SERAN combines a randomized and a deterministic approach. While the randomized component provides robustness over unreliable channels, the deterministic component avoids an explosion of packet collisions and allows our protocol to scale with network size. Our solution is based on a mathematical model that characterizes performance accurately without extensive simulations. SERAN is robust against node failures and clock drifts, supports data aggregation algorithms and is easily implementable in any of the existing hardware platforms. Although SERAN was designed for manufacturing plants applications, it can be used in any type of clustered topology. We consider a representative case study and we present simulation results to show SERAN efficiency Alvise Bonivento, Carlo Fischione, Alberto L. Sangiovanni-Vincentelli, Fabio Graziosi, Fortunato Santucci |
MASS | 3 |
| 2005 | A formal approach to system level design: metamodels and unified design environmentsabstractThe debate about efficient methods for hardware-software co-design has taken interesting turns over the years. In this paper, we argue that the essential problems to solve are prior to the decision on how to partition the system in hardware-software. We present a formal platform-based design method we have proposed over the years and a design environment, Metropolis, supporting the methodology, which starts by capturing the design specifications at the highest level of abstraction and then proceed toward an efficient implementation by subsequent refinement steps. We present the modeling strategy used in Metropolis based on formal semantics that is general enough to support the models of computation proposed so far and that facilitates the creation of new ones. Nonfunctional and declarative constraints can also be captured using a logic language. Felice Balarin, Roberto Passerone, Alessandro Pinto, Alberto L. Sangiovanni-Vincentelli |
MEMOCODE | 4 |
| 2005 | An embedded system for an eye-detection sensor
Arnon Amir, Lior Zimet, Alberto L. Sangiovanni-Vincentelli, Sean Kao |
Comput. Vis. Image Underst. | 3 |
| 2005 | EditorialabstractAs embedded systems activities are increasingly being recognized as a single coherent endeavor, it is not surprising that those concerned with education are striving to define appropriate curricula for this emerging engineering discipline.In this special issue of the Transactions on Embedded Systems, we focus on university education.We provide examples of existing practices, look at initiatives to develop new curricula, and take an educationally centered view on the evolution of this new engineering domain.Although there is a significant and growing agreement as to what defines embedded systems engineering, there is not a universal consensus as to what constitutes the discipline boundaries and, hence, what should be covered in "university provision."This special issue is, therefore, of interest to those involved in education and those interested in the development of the discipline itself.Industrial practice constrains this development, but so does the knowledge base and skills that graduates obtain.Indeed, it is perhaps only possible within universities to take a holistic view of any engineering discipline to define its core topics, necessary foundations, and linked themes.In this special issue eight papers are presented.Four describe experiences gained from teaching (partially or completely) embedded systems as a distinct subject and are from United States institutions that are well known for their research work in embedded systems. 1 What is of interest here is not only what is taught, but how the required teaching is organized.Important issues are the balance between formal lectures and project work, between student-centered and class-based learning, between theory and practice, and between methods and tools.The first paper describes the courses in embedded systems at the University of California at Berkeley with particular emphasis on the graduate curriculum.Their guiding principle is to bring together system theory and computer science.The curriculum has been growing since 1988 out of a bottom-up approach typical of U.S. institutions and is spread over a number of experimental and established courses that provide the foundation from which a future graduate and undergraduate program in embedded systems will rise as a coherent whole.At the CMU, an undergraduate course has evolved over the last three decades.Key areas covered are small and single microprocessor applications, control systems, distributed embedded control, system on chip, networking, embedded PCs, critical systems, robotics, computer peripherals, wireless data systems, signal processing, and command and control.Additional cross-cutting Alan Burns 0001, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2005 | Guidelines for a graduate curriculum on embedded software and systemsabstractThe design of embedded real-time systems requires skills from multiple specific disciplines, including, but not limited to, control, computer science, and electronics. This often involves experts from differing backgrounds, who do not recognize that they address similar, if not identical, issues from complementary angles. Design methodologies are lacking in rigor and discipline so that demonstrating correctness of an embedded design, if at all possible, is a very expensive proposition that may delay significantly the introduction of a critical product. While the economic importance of embedded systems is widely acknowledged, academia has not paid enough attention to the education of a community of high-quality embedded system designers, an obvious difficulty being the need of interdisciplinarity in a period where specialization has been the target of most education systems. This paper presents the reflections that took place in the European Network of Excellence Artist leading us to propose principles and structured contents for building curricula on embedded software and systems. Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Luís Almeida 0001, Albert Benveniste, Bruno Bouyssounouse, Giorgio C. Buttazzo, Ivica Crnkovic, Werner Damm, Jakob Engblom, Gerhard Fohler, Marisol García-Valls, Hermann Kopetz, Yassine Lakhnech, François Laroussinie, Luciano Lavagno, Giuseppe Lipari, Florence Maraninchi, Philipp Peti, Juan Antonio de la Puente, Norman Scaife, Joseph Sifakis, Robert de Simone, Martin Törngren, Paulo Veríssimo, Andy J. Wellings, Reinhard Wilhelm, Tim A. C. Willemse, Wang Yi 0001 |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2005 | An overview of embedded system design education at berkeleyabstractEmbedded systems have been a traditional area of strength in the research agenda of the University of California at Berkeley. In parallel to this effort, a pattern of graduate and undergraduate classes has emerged that is the result of a distillation process of the research results. In this paper, we present the considerations that are driving our curriculum development and we review our undergraduate and graduate program. In particular, we describe in detail a graduate class (EECS249: Design of Embedded Systems: Modeling, Validation and Synthesis) that has been taught for six years. A common feature of our education agenda is the search for fundamentals of embedded system science rather than embedded system design techniques, an approach that today is rather unique. Alberto L. Sangiovanni-Vincentelli, Alessandro Pinto |
ACM Trans. Embed. Comput. Syst. | 1 |
| 2004 | The best of both worlds: the efficient asynchronous implementation of synchronous specificationsabstractThe desynchronization approach combines a traditional synchronous specification style with a robust asynchronous implementation model. The main contribution of this paper is the description of two optimizations that decrease the overhead of desynchronization. First, we investigate the use of clustering to vary the granularity of desynchronization. Second, by applying temporal analysis on a formal execution model of the desynchronized design, we uncover significant amounts of timing slack. These methods are successfully applied to industrial RTL designs. Abhijit Davare, Kelvin Lwin, Alex Kondratyev, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 2004 | Benefits and challenges for platform-based designabstractPlatforms have become an important concept in the design of electronic systems. We present here the motivations behind the interest shown and the challenges that we have to face to make the Platform-based Design method a standard. As a generic term, platforms have meant different things to different people. The main challenges are to distill the essence of the method, to formalize it and to provide a framework to support its use in areas that go beyond the original domain of application. Alberto L. Sangiovanni-Vincentelli, Luca P. Carloni, Fernando De Bernardinis, Marco Sgroi |
DAC | 1 |
| 2004 | A Methodology for System-Level Analog Design Space ExplorationabstractThis paper describes a novel approach to system level analog design. A new abstraction level - the platform - is introduced to separate circuit design from design space exploration. An analog platform encapsulates analog components concurrently modeling their behavior and their achievable performances. Performance models are obtained through statistical sampling of circuit configurations. The design configurations space is specified with analog constraint graphs so that the sampling space is significantly reduced. System level exploration can be achieved through optimization on behavioral models constrained by performance models. Finally, an example is provided showing the effectiveness of the approach on a WCDMA amplifier. Fernando De Bernardinis, Alberto L. Sangiovanni-Vincentelli |
DATE | 2 |
| 2004 | Microarchitecture Development via Metropolis Successive Platform RefinementabstractProductivity data for IC designs indicates an exponential increase in design time and cost with the number of elements that are to be included in a device. Present applications require the development of complex systems to support novel functionality. To cope with these difficulties, we need to change radically the present design methodology to allow for extensive re-use, early verification in the design cycle, pervasive use of software, and architecture-level optimization. Platform-based design as defined in A. Sangiovanni-Vincentelli (2002), has these characteristics. We present the application of this methodology to a complex industrial application provided by Cypress Semiconductor. In this case study, we focus on a particular aspect of this methodology that eases considerably the verification process: successive refinement. We compare this approach versus a parallel team of designers who developed the IC using standard design approaches. Douglas Densmore, Sanjay Rekhi, Alberto L. Sangiovanni-Vincentelli |
DATE | 3 |
| 2004 | Synthesis for Manufacturability: A Sanity CheckabstractAs we move towards nanometer technology, manufacturing problems become overwhelmingly difficult to solve. Presently, optimization for manufacturability is performed at a post-synthesis stage and has been shown capable of reducing manufacturing cost up to 10%. As in other cases, raising the abstraction layer where optimization is applied is expected to yield substantial gains. This paper focuses on a new approach to design for manufacturability: logic synthesis for manufacturability. This methodology consists of replacing the traditional area-driven technology mapping with a new manufacturability-driven one. We leverage existing logic synthesis tools to test our method. The results obtained by using STMicroelectronics 0.13 /spl mu/m library confirm that this approach is a promising solution for designing circuits with lower manufacturing cost, while retaining performance. Finally, we show that our synthesis for manufacturability can achieve even larger cost reduction when yield-optimized cells are added to the library, thus enabling a wider area-yield tradeoff exploration. Alessandra Nardi, Alberto L. Sangiovanni-Vincentelli |
DATE | 2 |
| 2004 | Fault-Tolerant Deployment of Embedded Software for Cost-Sensitive Real-Time Feedback-Control ApplicationsabstractDesigning cost-sensitive real-time control systems for safety-critical applications requires a careful analysis of the cost/coverage trade-offs of fault-tolerant solutions. This further complicates the difficult task of deploying the embedded software that implements the control algorithms on the execution platform that is often distributed around the plant (as it is typical, for instance, in automotive applications). We propose a synthesis-based design methodology that relieves the designers from the burden of specifying detailed mechanisms for addressing platform faults, while involving them in the definition of the overall fault-tolerance strategy. Thus, they can focus on addressing plant faults within their control algorithms, selecting the best components for the execution platform, and defining an accurate fault model. Our approach is centered on a new model of computation, fault tolerant data flows (FTDF), that enables the integration of formal validation techniques. Claudio Pinello, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
DATE | 3 |
| 2004 | Heterogeneous reactive systems modeling: capturing causality and the correctness of loosely time-triggered architectures (LTTA)abstractWe present an extension of a mathematical framework proposed by the authors to deal with the composition of heterogeneous reactive systems. Our extended framework encompasses diverse models of computation and communication such as synchronous, asynchronous, causality-based partial orders, and earliest execution times. We introduce an algebra of tag structures and morphisms between tag sets to define heterogeneous parallel composition formally and we use a result on pullbacks from category theory to handle properly the case of systems derived by composing many heterogeneous components. The extended framework allows us to establish theorems, from which design techniques for correct-by-construction deployment of abstract specifications can be derived. We illustrate this by providing a complete formal support for correct-by-construction distributed deployment of a synchronous design specification over an ltta medium. Albert Benveniste, Benoît Caillaud, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 5 |
| 2004 | Conservative approximations for heterogeneous designabstractEmbedded systems are electronic devices that function in the context of a real environment, by sensing and reacting to a set of stimuli. Because of their close interaction with the environment, and to simplify their design, different parts of an embedded system are best described using different notations and different techniques. In this case, we say that the system is heterogeneous.We informally refer to the notation and the rules that are used to specify and verify the elements of heterogeneous system and their collective behavior as a model of computation. In this paper, we focus in particular on abstraction and refinement relationships in the form of conservative approximations. We do so by constructing a framework, called Agent Algebra, where the different models reside and share a common algebraic structure. We compare our techniques to the well established notion of abstract interpretation. We show that, unlike abstract interpretations, conservative approximations preserve refinement verification results from an abstract to a concrete model while avoiding false positives. In addition, we use the inverse of a conservative approximation to identify components that can be used indifferently in several models, thus enabling reuse across domains of computation. Roberto Passerone, Jerry R. Burch, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 3 |
| 2004 | Separation of concerns: overhead in modeling and efficient simulation techniquesabstractSeparating the description of important aspects of a design such as behavior and architecture, or computation and communication, may yield significant advantages in design time as well as in re-usability of the design. However, exploiting fully the re-usability opportunities offered by this approach implies to keep the various aspects of the design separated while verifying the design at a given level of abstraction. In particular, simulation of the design may undergo significant overhead versus a traditional approach where the design is represented and analyzed monolithically. In this paper, we present a few techniques that eliminate almost entirely the overhead while maintaining the positive aspects of the separation of concerns. Experimental results on a complex design back this assertion. Guang Yang 0004, Alberto L. Sangiovanni-Vincentelli, Yosinori Watanabe, Felice Balarin |
EMSOFT | 2 |
| 2004 | Adaptive sleep discipline for energy conservation and robustness in dense sensor networksabstractThis paper presents an adaptive approach for conserving energy in high-density sensor networks. The proposed method allows sensor nodes to sleep while ensuring that application performance constraints are met. Unlike deterministic algorithms that assume static connectivity, the approach uses a randomized algorithm to provide robustness to the variations in network connectivity. These variations are due to fading channels, depletion or addition of nodes, node mobility, and the sleeping of nodes. The algorithm developed in the paper is extremely lightweight and does not require nodes to keep any state information about their individual neighbors. Based on local observations, each node independently decides when to sleep and wakeup. The algorithm also ensures an evenly distributed workload among nodes, and achieves energy savings proportional to the density of nodes. Jana van Greunen, Dragan Petrovic, Alvise Bonivento, Jan M. Rabaey, Kannan Ramchandran, Alberto L. Sangiovanni-Vincentelli |
ICC | 6 |
| 2004 | SPFD-based wire removal in standard-cell and network-of-PLA circuitsabstractWire removal is a technique by which the total number of wires between individual circuit nodes is reduced, either by removing wires or replacing them with other new wires. The wire removal techniques we describe in this paper are based on both binary and multivalued sets of pairs of functions to be distinguished (SPFDs). Recently, it was shown that a design style based on a multilevel network of approximately equal-sized programmable logic arrays (PLAs) results in a dense, fast, and crosstalk-resistant layout. This paper describes the application of SPFD-based wire removal techniques for circuit implementations utilizing networks of PLAs as well as standard-cells. In our first set of wire removal experiments (which utilize binary SPFD-based wire removal), we demonstrate that the benefit of SPFD-based wire removal is insignificant when the circuit is mapped using standard cells. We demonstrate that this technique is very effective in the context of a network of PLAs. In the next set of wire removal experiments, we focus only on circuits implemented using a network of PLAs. Three separate wire removal experiments are performed. Wire removal is invoked before clustering the original netlist into a network of PLAs, or after clustering, or both before and after clustering. For wire removal before clustering, binary SPFD-based wire removal is used. For wire removal after clustering, multivalued SPFD-based wire removal is used since the multioutput PLAs can be viewed as multivalued single output nodes. We demonstrate that these techniques are effective. The most effective approach is to perform wire removal both before and after clustering. Using these techniques, we obtain a reduction in placed and routed circuit area of about 11%. This reduction is significantly higher (about 20%) for the larger circuits we used in our experiments. Sunil P. Khatri, Subarnarekha Sinha, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 2003 | Fault-tolerant platforms for automotive safety-critical applicationsabstractFault-tolerant electronic sub-systems are becoming a standard requirement in the automotive industrial sector as electronics becomes pervasive in present cars. We address the issue of fault tolerant chip architectures for automotive applications. We begin by reviewing fault-tolerant architectures commonly used in other industrial domains where fault-tolerant electronics has been a must for a number of years, e.g., the aircraft manufacturing industrial sector. We then proceed to investigate how these architecture could be implemented on a single chip and we compare them with a metric that combines traditional terms such as cost, performance and fault coverage with flexibility, i.e. the ability of adapting to changing requirements and capturing a wide range of applications, an emerging criterion for platform design. Finally, we describe in some details a cost effective dual lock-step platform that can be used as a single fail-operational unit or as two fail-silent channels trading fault-tolerance for performance. Massimo Baleani, Alberto Ferrari, Leonardo Mangeruca, Alberto L. Sangiovanni-Vincentelli, Maurizio Peri, Saverio Pezzini |
CASES | 4 |
| 2003 | Support vector machines for analog circuit performance representationabstractThe use of Support Vector Machines (SVMs) to represent the performance space of analog circuits is explored. In abstract terms, an analog circuit maps a set of input design parameters to a set of performance figures. This function is usually evaluated through simulations and its range defines the feasible performance space of the circuit. In this paper, we directly model performance spaces as mathematical relations. We study approximation approaches based on two-class and one-class SVMs, the latter providing a better tradeoff between accuracy and complexity avoiding "curse of dimensionality" issues with 2-class SVMs. We propose two improvements of the basic one-class SVM performances: conformal mapping and active learning. Finally we develop an efficient algorithm to compute projections, so that top-down methodologies can be easily supported. Fernando De Bernardinis, Michael I. Jordan, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 2003 | A tool for describing and evaluating hierarchical real-time bus scheduling policiesabstractWe present a tool suite for building, simulating, and analyzing the results of hierarchical descriptions of the scheduling policy for modules sharing a bus in real-time applications. These schedules can be based on a variety of factors including characteristics of messages and time slicing and are represented in a hierarchical tree-like structure that specifies multiple levels of arbitration. This structure can describe many popular arbitration schemes. Our simulator evaluates the specified scheduling structure on a set of message traces for a given bus. We illustrate our approach by applying it to two examples: the SAE Automotive Benchmark and Voice Over IP (VoIP). Although this paper deals with just bus scheduling policies, the approach can be easily extended to other real-time scheduling problems. Trevor Meyerowitz, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 2003 | System Level Design of Embedded Controllers: Knock Detection, A Case Study in the Automotive DomainabstractWe present a case study in the design of automotive engine controllers: the development of a knock detection algorithm and its implementation in an optimized platform. The design problem is complicated by the need of using heterogeneous models of computation and different design environments. The use of different design environments, one for functional design and one for architectural design space exploration, requires to transform a model of computation into another We describe how we solved this problem and we present the final design with the trade-offs explored. Leonardo Mangeruca, Alberto Ferrari, Alberto L. Sangiovanni-Vincentelli, Andrea Pierantoni, Michele Pennese |
DATE | 3 |
| 2003 | Equisolvability of Series vs. Controller's Topology in Synchronous Language Equations
Nina Yevtushenko 0001, Tiziano Villa, Robert K. Brayton, Alexandre Petrenko, Alberto L. Sangiovanni-Vincentelli |
DATE | 5 |
| 2003 | Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment
Albert Benveniste, Luca P. Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 4 |
| 2003 | A Methodology for the Computation of an Upper Bound on Nose Current Spectrum of CMOS Switching Activity
Alessandra Nardi, Haibo Zeng 0001, Joshua L. Garrett, Luca Daniel, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 5 |
| 2003 | Efficient Synthesis of Networks On ChipabstractWe propose an efficient heuristic for the constraint-driven communication synthesis (CDCS) of on-chip communication networks. The complexity of the synthesis problems comes from the number of constraints that have to be considered. We propose to cluster constraints to reduce the number that needs to be considered by the optimization algorithm. Then a quadratic programming approach is used to solve the communication synthesis problem with the clustered constraints. We provide an analytical model that justifies our choice of the clustering cost function and we discuss a set of experiments showing the effectiveness of the overall approach with respect to the exact algorithm. Alessandro Pinto, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
ICCD | 3 |
| 2003 | Structural Detection of Symmetries in Boolean FunctionsabstractFunctional symmetries provide significant benefits for multiple tasks in synthesis and verification. Many applications require the manual specification of symmetries using special language features such as symmetric data types. Methods for automatically detecting symmetries are based on functional analysis, e.g. using BDDs, or structural methods. The latter search for circuit graph automorphisms which imply functional symmetry. We present a method for finding symmetries of Boolean functions based on a two-step approach. First, the circuit structure is modified to maximize its structural regularity and thus the number of inherent automorphisms. The next step implements a fast algorithm for detecting the automorphism generators of the circuit graph. The generators provide a compact representation of all automorphisms, which in turn encode a subset of the functional symmetries. Because of its pure structural nature, our approach avoids the complexity issues inherent to methods using BDDs, yet it still works automatically and independently from the input specification format. However, the described method may not detect all functional symmetries, however, our experiments demonstrate that it can find the majority of the symmetries present in practical circuits. Andreas Kuehlmann, Alberto L. Sangiovanni-Vincentelli |
ICCD | 3 |
| 2003 | Low power coordination in wireless ad-hoc networksabstractDistributed wireless ad-hoc networks (DWANs) pose numerous technical challenges. Among them, two are widely considered as crucial: autonomous localized operation and minimization of energy consumption. We address the fundamental problem of how to maximize life-time of the network by using only local information while preserving network connectivity. We start by introducing the Care-Free Sleep (CS) Theorem that provides provably optimal necessary and sufficient conditions for a node to turn off its radio while ensuring that global connectivity is not affected.The CS theorem is the basis for an efficient localized algorithm that decides which node will turn its radio off, and for how long. The effectiveness of the approach is demonstrated using numerous simulations of the performance of the algorithm over a wide range of network parameters. Farinaz Koushanfar, Abhijit Davare, Dai Tho Nguyen, Miodrag Potkonjak, Alberto L. Sangiovanni-Vincentelli |
ISLPED | 5 |
| 2003 | Platform-based embedded software design and system integration for autonomous vehiclesabstractAutomatic control systems typically incorporate legacy code and components that were originally designed to operate independently. Furthermore, they operate under stringent safety and timing constraints. Current design strategies deal with these requirements and characteristics with ad hoc approaches. In particular, when designing control laws, implementation constraints are often ignored or cursorily estimated. Indeed, costly redesigns are needed after a prototype of the control system is built because of missed timing constraints and subtle transient errors. In this paper, we use the concepts of platform-based design to develop a methodology for the design of automatic control systems that builds in modularity and correct-by-construction procedures. We illustrate our strategy by describing the (successful) application of the methodology to the design of a time-based control system for a helicopter-based uninhabited aerial vehicle. Benjamin Horowitz, Judith Liebman, Cedric Ma, Tak-John Koo, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry |
Proc. IEEE | 5 |
| 2002 | Constraint-driven communication synthesisabstractConstraint-driven Communication Synthesis enables the automatic design of the communication architecture of a complex system from a library of pre-defined Intellectual Property (IP) components. The key communication parameters that govern all the point-to-point interactions among system modules are captured as a set of arc constraints in the communication constraint graph. Similarly, the communication features offered by each of the components available in the IP communication library are captured as a set of feature resources together with its cost figures. Then, every communication architecture that can be built using the available components while satisfying all constraints is implicitly considered (as an implementation graph matching the constraint graph) to derive the optimum design solution with respect to the desired cost figure. The corresponding constrained optimization problem is efficiently solved by a novel algorithm that is presented here together with its rigorous theoretical foundations. Alessandro Pinto, Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 2002 | Compositional Modeling in Metropolis
Gregor Gößler, Alberto L. Sangiovanni-Vincentelli |
EMSOFT | 2 |
| 2002 | Platform-Based Embedded Software Design for Multi-vehicle Multi-modal Systems
Tak-John Koo, Judith Liebman, Cedric Ma, Benjamin Horowitz, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry |
EMSOFT | 5 |
| 2002 | An Enhanced POLIS Framework for Fast Exploration and Implementation of I/O Subsystems on CSoC Platforms
Massimo Baleani, Massimo Conti, Alberto Ferrari, Valerio Frascolla, Alberto L. Sangiovanni-Vincentelli |
FPL | 5 |
| 2002 | Proximity templates for modeling of skin and proximity effects on packages and high frequency interconnectabstractModeling the exponentially varying current distributions in conductor interiors associated with high frequency interconnect behavior causes a rapid increase in the computation time and memory required even by recently developed fast electromagnetic analysis programs. In this paper we describe a procedure to generate numerically a set of basis functions which efficiently represent conductor current variation, and thus improving solver efficiency. The method is based on solving a sequence of template problems, and is easily generalized to arbitrary conductor cross-sections. Results are presented to demonstrate that the numerically computed basis functions are seven to twenty times more efficient than the commonly used piece-wise constant basis functions. Luca Daniel, Alberto L. Sangiovanni-Vincentelli, Jacob K. White 0001 |
ICCAD | 2 |
| 2002 | Convertibility verification and converter synthesis: two faces of the same coinabstractAn essential problem in component-based design is how to compose components designed in isolation. Several approaches have been proposed for specifying component interfaces that capture behavioral aspects such as interaction protocols, and for verifying interface compatibility. Likewise, several approaches have been developed for synthesizing converters between incompatible protocols. In this paper, we introduce the notion of adaptability as the property that two interfaces have when they can be made compatible by communicating through a converter that meets specified requirements. We show that verifying adaptability and synthesizing an appropriate converter are two faces of the same coin: adaptability can be formalized and solved using a game-theoretic framework, and then the converter can be synthesized as a strategy that always wins the game. Finally we show that this framework can be related to the rectification problem in trace theory. Roberto Passerone, Luca de Alfaro, Thomas A. Henzinger, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 2002 | Models of IP's for Automotive Virtual Integration PlatformsabstractSummary form only given.The concept of virtual integration platform plays a key role in any novel methodology that is trying to address earlier validation of distributed applications in regular and faulty conditions. The methodology must rely upon libraries that model the most important features of the commonly used IP's in the automotive segment such as FlexRay, the emerging bus protocol for safety critical applications supported by BMW, Daimler-Chrysler, Philips, Bosch, and Motorola, OSEK compliant RTOSes and protocol stacks, microprocessors such as Motoro/IBM PowerPC, Infineon 167, NEC v850, Tricore, ST 10, and Janus. We believe that tools must support the easy plug and play of the IP models in a seamless way to the user. For example, it must be possible to run a fast simulation at the token level (frames) to provide insights about the best network protocol configuration within a reasonable accuracy for the estimated frame latency. Next, it must be possible to export such a configuration to (semi)-automatically configure the downstream and more refined bus protocol models for the finer grain validation step. Both steps must rely upon interchangeable IP's with clear interfaces and trade-offs between simulation speed and accuracy of the timing estimates. In this paper, we present two examples of models of IP's that can be used at two different steps in the design exploration, the token-level/cycle approximate transaction based level and the cycle accurate level. The first example is the Universal Communication Model (UCM) that captures the main common features of the most relevant bus protocols such as topology, redundancy, arbitration, etc. The model enables quick token-level simulations. The user is able to determine the communication cycle layout and bus scheduling, k-matrix, and then export it for the configuration of downstream more refined models such as the Motorola FlexRay cycle accurate transaction based model. Bus delays are as important as task execution delays and RTOS switching overheads. In the second example we introduce Janus, a multi-processor micro-controller for power train applications. The cycle approximate transaction based model of Janus can be used to assess the ECU HW/SW partitioning, in particular to quickly explore different task scheduling and allocation. Then, this model is refined and exported to configure a HW/SW co-verification tool for the cycle accurate validation of the ECU HW/SW architecture. In an example scenario, an engine control ECU is providing information about the engine (e.g. engine revolution speed) to a gear control ECU over a CAN bus (the latter typically requires precise revolution speed to operate and could also require to set the engine operation condition). In this scenario, car and subsystem makers play different roles in order to provide a virtual model of the system to validate the functionality and the performance before going to implementation. The same models can then be used to march toward implementation. Paolo Giusto, Jean-Yves Brunel, Alberto Ferrari, Eliane Fourgeau, Luciano Lavagno, Barry O'Rourke, Alberto L. Sangiovanni-Vincentelli, Emanuele Guasto |
ICCD | 7 |
| 2002 | Automotive Virtual Integration Platforms: Why's, What's, and How'sabstractIn this paper, we present the new concept of virtual integration platform for automotive electronics. The platform provides the basis for a novel methodology in which the integration of sub-systems is performed much earlier in the design cycle. As a result, cost reduction in the final implementation and in the design process can be achieved. In addition, early and repeatable fault analysis can be performed therefore easing the task of system safety proving. Paolo Giusto, Jean-Yves Brunel, Alberto Ferrari, Eliane Fourgeau, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
ICCD | 6 |
| 2002 | Formula-Dependent Equivalence for Compositional CTL Model Checking
Adnan Aziz, Thomas R. Shiple, Vigyan Singhal, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
Formal Methods Syst. Des. | 5 |
| 2001 | A vision for embedded softwareabstractIn this paper we describe a vision for the future evolution of Embedded SW (ESW) design methodologies as part of overall Embedded Systems (ES) development. Fundamentally, we believe that the way in which embedded SW is developed today must change radically. The key steps are: first, to link embedded software upwards in the abstraction layers to system functionality; and second, to link embedded software to the programmable platforms that support it. This will provide the much-needed means to verify whether the constraints posed on Embedded Systems are met. We envisage an optimised, automated, transparent and mathematically correct flow from product specification through to implementation for SW-dominated products implemented with highly programmable platforms. Alberto L. Sangiovanni-Vincentelli, Grant Martin |
CASES | 1 |
| 2001 | Using Conduction Modes Basis Functions for Efficient Electromagnetic Analysis of On-Chip and Off-Chip InterconnectabstractIn this paper, we present an efficient method to model the interior of the conductors in a quasi-static or full-wave integral equation solver. We show how interconnect cross-sectional current distributions can be modeled using a small number of conduction modes as basis functions for the discretization of the Mixed Potential Integral Equation (MPIE). Two examples are presented to demonstrate the computational attractiveness of our method. In particular, we show how our new approach can successfully and efficiently capture skin effects, proximity effects and transmission line resonances. Luca Daniel, Alberto L. Sangiovanni-Vincentelli, Jacob K. White 0001 |
DAC | 2 |
| 2001 | Addressing the System-on-a-Chip Interconnect Woes Through Communication-Based DesignabstractCommunication-based design represents a formal method approach to of system-on-a-chip design that considers communication between components as important as the computations they perform. “Our network-on-chip&rdqo ; approach partitions the communication into layers to maximize reuse and provide a programmer with an abstraction of the underlying communication framework. This layered approach is cast in the structure advocated by the OSI Reference network model and is demonstrated with a reconfigurable DSP example. The Metropolis methodology of deriving layers through a sequence of successive adaptation steps between incompatible behaviors refinement of communication is illustrated through the Intercom a design example. In another approach, MESCAL provides a designer with tools for a correct-by-construction protocol stack. Marco Sgroi, Michael Sheets, Andrew Mihal, Kurt Keutzer, Sharad Malik, Jan M. Rabaey, Alberto L. Sangiovanni-Vincentelli |
DAC | 7 |
| 2001 | Design methodology for PicoRadio networksabstractOne of the most compelling challenges of the next decade is the "last-meter" problem, extending the expanding data network into end-user data-collection and monitoring devices. PicoRadio supports the assembly of an ad hoc wireless network of self-contained mesoscale, low-cost, low-energy sensor and monitor nodes. While technology advances have made it conceivable to deploy wireless networks of heterogeneous nodes, the design of a low-power, low-cost, adaptive node in a reduced time to market is still a challenge. We present a design methodology for PicoRadio Networks, from system conception and optimization to silicon platform implementation. For each phase of the design, we demonstrate the applicability of our methodology through promising experimental results. Julio Leao da Silva Jr., J. Shamberger, M. Josie Ammer, Chunlong Guo, Suet-Fei Li, Rahul C. Shah, Tim Tuan, Michael Sheets, Jan M. Rabaey, Borivoje Nikolic, Alberto L. Sangiovanni-Vincentelli, Paul K. Wright |
DATE | 11 |
| 2001 | Techniques for Including Dielectrics when Extracting Passive Low-Order Models of High Speed InterconnectabstractInterconnect structures including dielectrics can be modeled by an integral equation method using volume currents and surface charges for the conductors, and volume polarization currents and surface charges for the dielectrics. In this paper we describe a mesh analysis approach for computing the discretized currents in both the conductors and the dielectrics. We then show that this fully mesh-based formulation can be cast into a form using provably positive semidefinite matrices, making for easy application of Krylov-subspace based model-reduction schemes to generate accurate guaranteed passive reduced-order models. Several printed circuit board examples are given to demonstrate the effectiveness of the strategy. Luca Daniel, Alberto L. Sangiovanni-Vincentelli, Jacob K. White 0001 |
ICCAD | 2 |
| 2001 | Addressing the Timing Closure Problem by Integrating Logic Optimization and PlacementabstractTiming closure problems occur when timing estimates computed during logic synthesis do not match with timing estimates computed from the layout of the circuit. In such a situation, logic synthesis and layout synthesis are iterated until the estimates match. The number of such iterations is becoming larger as technology scales. Timing closure problems occur mainly due to the difficulty in accurately predicting interconnect delay during logic synthesis. In this paper, we present an algorithm that integrates logic synthesis and global placement to address the timing closure problem. We introduce technology independent algorithms as well as technology dependent algorithms. Our technology independent algorithms are based on the notion of "wire-planning". All these algorithms interleave their logic operations with local and incremental/full global placement, in order to maintain a consistent placement while the algorithm is run. We show that by integrating logic synthesis and placement, we avoid the need to predict interconnect delay during logic synthesis. We demonstrate that our scheme significantly enhances the predictability of wire delays, thereby solving the timing closure problem. This is the main result of our paper. Our results also show that our algorithms result in a significant reduction in total circuit delay. In addition, our technology independent algorithms result in a significant circuit area reduction. Wilsin Gosti, Sunil P. Khatri, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 2001 | System-Level Power/Performance Analysis of Portable Multimedia Systems Communicating over Wireless ChannelsabstractThis paper presents a new methodology for system-level power and performance analysis of wireless multimedia systems. More precisely, we introduce an analytical approach based on concurrent processes modeled as Stochastic Automata Networks (SANs) that can be effectively used to integrate power and performance metrics in system-level design. We show that 1) under various input traces and wireless channel conditions, the average-case behavior of a multimedia system consisting of a video encoder/decoder pair is characterized by very different probability distributions and power consumption values and 2) in order to identify the best trade-off between power and performance figures, one must take into consideration the entire environment (i.e., encoder, decoder and channel) for which the system is being designed. Compared to using simulation, our analytical technique reduces the time needed to find the steady-state behavior by orders of magnitude, with some limited loss in accuracy compared to the exact solution. We illustrate the potential of our methodology using the MPEG-2 video as the driver application. Radu Marculescu, Amit Nandi, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 2001 | Solution of Parallel Language Equations for Logic SynthesisabstractThe problem of designing a component that, combined with a known part of a system, conforms to a given overall specification arises in several applications ranging from logic synthesis to the design of discrete controllers. We cast the problem as solving abstract equations over languages. Language equations can be defined with respect to several language composition operators such as synchronous composition, /spl middot/, and parallel composition, /spl square/; conformity can be checked by language containment. In this paper, we address parallel language equations. Parallel composition arises in the context of modeling delay-insensitive processes and their environments. The parallel composition operator models an exchange protocol by which an input is followed by an output after a finite exchange of internal signals. It abstracts a system with two components with a single message in transit, such that at each instance either the components exchange messages or one of them communicates with its environment, which submits the next external input to the system only after the system has produced an external output in response to the previous input. We study the most general solutions of the language equation A/spl square/X/spl sube/C, and define the language operators needed to express them. Then we specialize such equations to languages associated with important classes of automata used for modeling systems, e.g., regular languages and FSM languages. In particular, for A/spl square/X/spl sube/C, we give algorithms for computing: the largest FSM language solution, the largest complete solution, and the largest solution whose composition with A yields a complete FSM language. We solve also FSM equations under bounded parallel composition. In this paper, we give concrete algorithms for computing such solutions, and state and prove their correctness. Nina Yevtushenko 0001, Tiziano Villa, Robert K. Brayton, Alexandre Petrenko, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 5 |
| 2001 | Embedded Software Design for Real-Time Applications
Alberto L. Sangiovanni-Vincentelli |
RTSS | 1 |
| 2001 | Limitations and challenges of computer-aided design technology for CMOS VLSIabstractAs manufacturing technology moves toward fundamental limits of silicon CMOS processing, the ability to reap the full potential of available transistors and interconnect is increasingly important. Design technology (DT) is concerned with the automated or semi-automated conception, synthesis, verification, and eventual testing of microelectronic systems. While manufacturing technology faces fundamental limits inherent in physical laws or material properties, design technology faces fundamental limitations inherent in the computational intractability of design optimizations and in the broad and unknown range of potential applications within various design processes. In this paper, we explore limitations to how design technology can enable the implementation of single-chip microelectronic systems that take full advantage of manufacturing technology with respect to such criteria as layout density performance, and power dissipation. Randal E. Bryant, Kwang-Ting Cheng, Andrew B. Kahng, Kurt Keutzer, Wojciech Maly, A. Richard Newton, Lawrence T. Pileggi, Jan M. Rabaey, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 9 |
| 2001 | Theory of latency-insensitive designabstractThe theory of latency-insensitive design is presented as the foundation of a new correct-by-construction methodology to design complex systems by assembling intellectual property components. Latency-insensitive designs are synchronous distributed systems and are realized by composing functional modules that exchange data on communication channels according to an appropriate protocol. The protocol works on the assumption that the modules are stallable, a weak condition to ask them to obey. The goal of the protocol is to guarantee that latency-insensitive designs composed of functionally correct modules behave correctly independently of the channel latencies. This allows us to increase the robustness of a design implementation because any delay variations of a channel can be "recovered" by changing the channel latency while the overall system functionality remains unaffected. As a consequence, an important application of the proposed theory is represented by the latency-insensitive methodology to design large digital integrated circuits by using deep submicrometer technologies. Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2001 | Synchronous approach to the functional equivalence of embeddedsystem implementationsabstractDesign space exploration is the process of analyzing several functionally equivalent alternatives to determine the most suitable one. A fundamental question is whether an implementation is consistent with the high-level specification or whether two implementations are "equivalent." The synchronous assumption has made it possible to develop efficient procedures for establishing functional equivalence between different implementations in the domains of synchronous circuits and synchronous reactive systems. We extend this notion to embedded systems that do not satisfy the synchronous assumption inside their boundaries but only at the interface with the environment. Leveraging this property, we define synchronous equivalence for embedded systems that strongly resembles the concept of functional equivalence for sequential circuits. We develop efficient synchronous equivalence analysis algorithms for embedded system designs. The efficiency comes from analyzing the behavior statically on abstract representations, at a cost that some of the negative results may be false, i.e. the analysis is conservative. We develop primitives for making the representation more/less abstract, trading off complexity of the algorithms with the conservativeness of the results. We apply our analysis algorithms to an ATM switch and demonstrate that synchronous equivalence opens design exploration avenues uncharted before. Harry Hsieh, Felice Balarin, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 2000 | Formal Models for Communication-Based Design
Alberto L. Sangiovanni-Vincentelli, Marco Sgroi, Luciano Lavagno |
CONCUR | 1 |
| 2000 | Performance analysis and optimization of latency insensitive systemsabstractLatency insensitive design has been recently proposed in literature as a way to design complex digital systems, whose functional behavior is robust with respect to arbitrary variations in interconnect latency. However, this approach does not guarantee the same robustness for the performance of the design, which indeed can experience big losses. This paper presents a simple, yet rigorous, method to (1) model the key properties of a latency insensitive system, (2) analyze the impact of interconnect latency on the overall throughput, and (3) optimize the performance of the final implementation. Luca P. Carloni, Alberto L. Sangiovanni-Vincentelli |
DAC | 2 |
| 2000 | Task generation and compile-time scheduling for mixed data-control embedded softwareabstractThe problem of optimal software synthesis for concurrent processes to be implemented on a single processor is addressed. The approach calls for the representation of the concurrent processes with Petri nets that give a theoretical foundation for the scheduling algorithm that sequentializes the concurrent processes and for the code generation step. The approach maximizes the amount of static scheduling to reduce the need of context switch and operating system intervention. Experimental results show the potential of our method to reduce software design time and errors. Jordi Cortadella, Alex Kondratyev, Luciano Lavagno, Marc Massot, Sandra Moral, Claudio Passerone, Yosinori Watanabe, Alberto L. Sangiovanni-Vincentelli |
DAC | 8 |
| 2000 | Efficient methods for embedded system design space explorationabstractDesign space exploration is the process of analyzing several functionally equivalent alternatives to determine the most suitable one. The synchronous assumption has made it possible to develop efficient procedures for establishing functional equivalence between different implementations in the domain of synchronous circuits as well as in the domain of synchronous reactive systems. We extend this notion to embedded systems that do not satisfy the synchronous assumption inside their boundaries but only at the interface with the environment Leveraging this property, we developed efficient synchronous equivalence analysis algorithms for embedded systems with loops and architectures with multiple computational units. We demonstrate our method on an ATM switch containing many interacting components. Harry Hsieh, Felice Balarin, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 2000 | Embedded systems education (panel abstract)abstractThe design and design automation of embedded systems is rapidly emerging as a research area in its own right. It draws from several traditional areas of study such as system specification, modeling and analysis; computer architecture and micro-architecture; as well as compilers and operating systems. However, the embedded domain adds some interesting twists in terms of tighter problem constraints that demand a fresh look at even these traditional areas. In addition, there are several emerging EDA areas such as design reuse and integration of systems on a chip that are critical to the study of embedded systems. These aspects are not typically covered by computer engineering and EDA curricula. This panel addresses the challenges associated with the educational issues in embedded systems design and design automation. The panelists will examine issues in including embedded systems in university curricula, as well as in setting up research programs that are crucial for the education of graduate students. Sharad Malik, D. K. Arvind 0001, Edward A. Lee, Philip Koopman, Alberto L. Sangiovanni-Vincentelli, Marilyn Wolf |
DAC | 5 |
| 2000 | Task scheduling with RT constraintsabstractThis paper addresses the problem of schedu ling reactive real-time tran saction s(task groups) implementing a net work of extend ed Finite State Machines comm unicating asynchronously. Task instances are activated in response to internal and/or external ev ents.The objective is avoiding the loss of events exchanged by the tasks. This sc heduling problem has many similarities with the conventional formulation of real-tim e problems and yet it differs enough to justify a rethinking of the assu mptions an d techniques used to solve the problem. Our iterative solution targets fixed p riority systems and offers a priority assignment scheme together with a sufficiently tight worst-case analysis. Marco Di Natale, Alberto L. Sangiovanni-Vincentelli, Felice Balarin |
DAC | 2 |
| 2000 | HW/SW Codesign of an Engine Management SystemabstractThe design process for an engine management system is presented. The functional specification of the system has been captured using C and C++ as specification languages. The validation of the specification has been carried out using functional simulation. Then an architecture for the implementation of the functional specification is selected among a set of three possible alternatives, all based on the same micro-controller; characterized by different hardware-software trade-offs. The choice is motivated by a fast performance estimation that can also be used to identify the parts of the design that could be moved across the hardware-software partition to obtain better cost or better performance. The case study has been performed in the Felix VCC framework. Massimo Baleani, Alberto Ferrari, Alberto L. Sangiovanni-Vincentelli, Claudio Turchetti |
DATE | 3 |
| 2000 | Free MDD-Based Software Optimization Techniques for Embedded SystemsabstractEmbedded systems make a heavy use of software to perform real-time embedded control tasks. Embedded software is characterized by a relatively long lifetime and by tight cost, performance and safety constraints. Several super-optimization techniques for embedded softwares based on multi-valued decision diagram (MDD) representations have been described in the literature, but they all share the same basic limitation. They are based on standard ordered MDD (OMDD) packages, and hence require a used order of evaluation for the MDD variables on every execution path. Free MDDs (FMDDs) lift this limitation, and hence open up more optimization opportunities. Finding the optimal variable ordering for FMDDs is a very difficult problem. Hence in this paper we describe a heuristic procedure that performs well in practice, and is based on FMDD cost estimation applied to recursive cofactoring. Experimental results show that our new variable ordering method obtains often. Smaller embedded software than previous (sifting-based) methods. Chunghee Kim, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
DATE | 3 |
| 2000 | Designing wireless protocols: methodology and applicationsabstractCommunication protocols are essential components of wireless systems. Present methods for protocol design are heuristic in nature and are not suited for next generation wireless systems where time-to-market concerns require correct-the-first-time implementations. In this paper we present a new design methodology for wireless protocols based on the principle of orthogonalization of concerns. In particular, the methodology separates function and architecture design and emphasizes the use of formal models to ensure correctness and reduce design time. Protocols are described using co-design finite state machines (CFSMs), a model of computation that has been introduced to allow the efficient capture of both the control and the data processing parts of the specification. Furthermore, algorithms for automatic hardware and software synthesis from CFSMs are available. This allows a fast exploration of different HW/SW partitions and the analysis of tradeoffs involved. Intercom, a mobile wireless system supporting full-duplex voice communication among different users, is presented and the design of its protocols is described. The design methodology presented here will be used for the design of PicoRadio, a low-power and highly adaptive network of sensors. Marco Sgroi, Julio Leao da Silva Jr., Fernando De Bernardinis, Fred L. Burghardt, Alberto L. Sangiovanni-Vincentelli, Jan M. Rabaey |
ICASSP | 5 |
| 2000 | Cross-Talk Immune VLSI Design Using a Network of PLAs Embedded in a Regular Layout FabricabstractWe present a VLSI design methodology to address the cross-talk problem, which is becoming increasingly important in Deep Sub-Micron (DSM) IC design. In our approach, we implement the logic netlist in the form of a network of medium sized PLAs. We utilize two regular layout "fabrics" in our methodology, one for areas where PLA logic is implemented, and another for routing regions between such logic blocks. We show that a single PLA implemented in the first fabric style is not only cross-talk immune, but also about 2/spl times/ smaller and faster than a traditional standard cell based implementation of the same logic. The second fabric, utilized in the routing region between individual PLAs, is also highly cross-talk immune. Additionally, in this fabric, power and ground signals are essentially "pre-routed" all over the die. Our synthesis flow involves decomposing the design into a network of PLAs, each of which has a bounded width and height. The number of inputs and outputs of each PLA are flexible as long as the resulting PLA width is bounded. We perform folding of PLAs to achieve better logic density. Routing is performed using 2,3,4,5 and 6 routing layers. State-of-the-art commercial routing tools are utilized for the experiments involving the use of 3,4,5 and 6 routing layers. We have implemented the entire design flow using these ideas. Our scheme results in a reduction in the cross-talk between signal wires of between one and two orders of magnitude. As a result, for a 0.1 /spl mu/m process, the delay variation due to cross-talk dramatically drops from 2.47:1 to 1.02:1. Additionally, our methodology results in circuits that are extremely fast and dense, with a timing improvement of about 15% and an overall area penalty of about 3% compared to standard cells. The regular arrangement of metal conductors in our scheme results in low and highly predictable inductive and capacitive parasitics, resulting in highly predictable designs. The crosstalk immunity, high speed, low area overhead and high predictability of our methodology indicate that it is a strong candidate as the preferred design methodology in the DSM era. Sunil P. Khatri, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 2000 | Binary and Multi-Valued SPFD-Based Wire Removal in PLA NetworksabstractThis paper describes the application of binary and multivalued SPFD-based wire removal techniques for circuit implementations utilizing networks of PLAs. It has been shown that a design style based on a multi-level network of approximately equal-sized PLAs results in a dense, fast, and crosstalk-resistant layout. Wire removal is a technique where the total number of wires between individual circuit nodes is reduced, either by removing wires, or replacing them with other existing wires. Three separate wire removal experiments are performed. Either wire removal is invoked before clustering the original netlist into a network of PLAs, or after clustering, or both before and after clustering. For wire removal before clustering, binary SPFD-based wire removal is used. For wire removal after clustering, multi-valued SPFD-based wire removal is used since the multi-output PLAs can be viewed as multi-valued single output nodes. We demonstrate that these techniques are effective. The most effective approach is to perform wire removal both before and after clustering. Using these techniques, we obtain a reduction in placed and routed circuit area of about 11%. This reduction is significantly higher (about 20%) for the larger circuits we used in our experiments. Subarnarekha Sinha, Sunil P. Khatri, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCD | 4 |
| 2000 | Automotive engine control and hybrid systems: challenges and opportunitiesabstractThe design of engine control systems has been traditionally carried out using a mix of heuristic techniques validated by simulation and prototyping using approximate average-value models. However, the ever increasing demands on passengers' comfort, safety, emissions, and fuel consumption imposed by car manufacturers and regulations call for more robust techniques and the use of cycle-accurate models. We argue that these models must be hybrid because of the combination of time-domain and event-based behaviors. We present a hybrid model of the engine in which both continuous and discrete time-domain as well as event-based phenomena are modeled in a separate but integrated manner. Based on this model, we formalize the specification of the overall engine control by defining a number of hybrid control problems. To cope with the difficulties arising in the design of hybrid controllers, a design methodology is proposed. This methodology consists of a relaxation of the hybrid problem by simplifying some of its components to obtain a solvable problem,and then deriving a solution to the original control problem by appropriately modifying the control law so obtained to take into consideration the original specifications and models. The effectiveness of this approach is illustrated on three challenging problems: fast force-transient control, cutoff control, and idle speed control. Andrea Balluchi, Luca Benvenuti, Maria Domenica Di Benedetto, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 5 |
| 2000 | Sequential synthesis using S1SabstractWe propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this leads to simple and mathematically elegant solutions to problems arising in the synthesis and optimization of synchronous digital hardware. Specifically, we derive a logical expression which yields a single finite state automaton characterizing the set of implementations that can replace a component of a larger design. The power of our approach is demonstrated by the fact that it generalizes immediately to arbitrary interconnection topologies, and to designs containing nondeterminism and fairness. We also describe control aspects of sequential synthesis and relate controller realizability to classical work on program synthesis and tree automata. Adnan Aziz, Felice Balarin, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 2000 | Negative thinking in branch-and-bound: the case of unate coveringabstractWe introduce a new technique for solving some discrete optimization problems exactly. The motivation is that when searching the space of solutions by a standard branch-and-bound (B&B) technique, often a good solution is reached quickly and then improved only a few times before the optimum is found: hence, most of the solution space is explored to certify optimality, with no improvement in the cost function. This suggests that more powerful lower bounding would speed up the search dramatically. More radically, it would be desirable to modify the search strategy with the goal of proving that the given subproblem cannot yield a solution better than the current best one (negative thinking), instead of branching further in search for a better solution (positive thinking). For illustration we applied our approach to the unate covering problem. The algorithm starts in the positive-thinking mode by a standard B&B procedure that generates recursively smaller subproblems. If the current subproblem is "deep" enough, the algorithm switches to the negative thinking mode where it tries to prove that solving the subproblem does not improve the solution. The latter is achieved by a new search procedure invoked when the difference between the upper and lower bound is "small". Such a procedure is complete: either it yields a lower bound that matches the current upper bound, or it yields a new solution better than the current one. We implemented our new search procedure on top of ESPRESSO and SCHERZO, two state-of-art covering solvers used for computer-aided design applications, showing that in both cases we obtain new search engines (respectively, AURA and AURA II) much more efficient than the original ones. Eugene Goldberg, Luca P. Carloni, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 5 |
| 2000 | System-level design: orthogonalization of concerns andplatform-based designabstractSystem-level design issues become critical as implementation technology evolves toward increasingly complex integrated circuits and the time-to-market pressure continues relentlessly. To cope with these issues, new methodologies that emphasize re-use at all levels of abstraction are a "must", and this is a major focus of our work in the Gigascale Silicon Research Center. We present some important concepts for system design that are likely to provide at least some of the gains in productivity postulated above. In particular, we focus on a method that separates parts of the design process and makes them nearly independent so that complexity could be mastered. In this domain, architecture-function co-design and communication-based design are introduced and motivated. Platforms are essential elements of this design paradigm. We define system platforms and we argue about their use and relevance. Then we present an application of the design methodology to the design of wireless systems. Finally, we present a new approach to platform-based design called modern embedded systems, compilers, architectures and languages, based on highly concurrent and software programmable architectures and associated design tools. Kurt Keutzer, A. Richard Newton, Jan M. Rabaey, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1999 | Fast Instruction Cache Simulation Strategies in a Hardware/Software Co-Design EnvironmentabstractCache memories are one of the main factors that affect software performance, and their use is becoming increasingly common even in embedded systems. Efficient analysis of the effects of parameter variations (cache dimensions, degree of associativity, replacement policy, line size, ...) is at the same time an essential and very time-consuming aspect of embedded system design, whose complexity increases when multi-tasking and real-time aspects must be considered. We propose a new simulation-based methodology, focused on an approximate model of the cache and of the multi-tasking reactive software, that allows one to trade off smoothly between accuracy and simulation speed. In particular, we propose to accurately consider intra-task conflicts, but approximate inter-task conflicts by considering only a finite number of previous task executions. The rationale for this choice can be found in a common pattern in embedded systems, where a "normal" data flow results in a regular intra-task common flow, interrupted from time to time by some urgent event, that pessimistically can be consider as disrupting the cache behavior. The approach is conservative because re-execution of a task after a large amount of time will always be considered as not in cache, and the simulation speed-up is considerable, as shown by theoretical analysis and experimental results. Marcello Lajolo, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
ASP-DAC | 3 |
| 1999 | Latency Insensitive Protocols
Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli |
CAV | 3 |
| 1999 | On Thermal Effects in Deep Sub-Micron VLSI InterconnectsabstractArticle Free Access Share on On thermal effects in deep sub-micron VLSI interconnects Authors: Kaustav Banerjee Integrated Systems, Department of Electrical Engineering, Stanford University, Stanford, CA and Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA Integrated Systems, Department of Electrical Engineering, Stanford University, Stanford, CA and Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CAView Profile , Amit Mehrotra Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CAView Profile , Alberto Sangiovanni-Vincentelli Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CAView Profile , Chenming Hu Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CAView Profile Authors Info & Claims DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation ConferenceJune 1999Pages 885–891https://doi.org/10.1145/309847.310093Published:01 June 1999Publication History 60citation1,225DownloadsMetricsTotal Citations60Total Downloads1,225Last 12 Months111Last 6 weeks22 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Publisher SiteeReaderPDF Kaustav Banerjee, Amit Mehrotra, Alberto L. Sangiovanni-Vincentelli, Chenming Hu |
DAC | 3 |
| 1999 | HW and SW in Embedded System Design: Loveboat, Shipwreck, or Ships Passing in the NightabstractNo abstract available. Raúl Camposano, Kurt Keutzer, Jerry Fiddler, Alberto L. Sangiovanni-Vincentelli, Jim Lansford |
DAC | 4 |
| 1999 | A Novel VLSI Layout Fabric for Deep Sub-Micron ApplicationsabstractWe propose a new VLSI layout methodology which addresses the main problems faced in Deep Sub-Micron (DSM) integrated circuit design. Our layout “fabric ” scheme eliminates the conventional no-tion of power and ground routing on the integrated circuit die. In-stead, power and ground are essentially “pre-routed ” all over the die. By a clever arrangement of power/ground and signal pins, we almost completely eliminate the capacitive effects between signal wires. Ad-ditionally, we get a power and ground distribution network with a very low resistance at any point on the die. Another advantage of our scheme is that the arrangement of conductors ensures that on-chip inductances are uniformly negligible. Finally, characterization of the circuit delays, capacitances and resistances becomes extremely simple in our scheme, and needs to be done only once for a design. We show how the uniform parasitics of our fabric give rise to a reliable and predictable design. We have implemented our scheme using public domain layout software. Preliminary results show that it holds much promise as the layout methodology of choice in DSM integrated circuit design. 1 Sunil P. Khatri, Amit Mehrotra, Robert K. Brayton, Ralph H. J. M. Otten, Alberto L. Sangiovanni-Vincentelli |
DAC | 5 |
| 1999 | Fast Hardware-Software Co-simulation Using VHDL ModelsabstractWe describe a technique for hardware-software co-simulation that is almost cycle-accurate, and does nor require the use of interprocess communication for a C language interface for the software components. Software is modeled by using behavioral VHDL constructs, annotated with timing information derived from basic block-level timing estimates. Hardware is also modeled in VHDL, and can be either pre-existing intellectual property or synthesized to RTL from a functional specification. Execution of the VHDL processes modeling software tasks is coordinated by a process emulating the target RTOS behavior. The effects of changing the hardware/software partition can be quickly estimated by changing a process parameter defining its target implementation and the processor on which it is running. Bassam Tabbara, Marco Sgroi, Alberto L. Sangiovanni-Vincentelli, Enrica Filippi, Luciano Lavagno |
DATE | 3 |
| 1999 | A methodology for correct-by-construction latency insensitive designabstractIn deep sub-micron (DSM) designs, performance will depend critically on the latency of long wires. We propose a new synthesis methodology for synchronous systems that makes the design functionally insensitive to the latency of long wires. Given a synchronous specification of a design, we generate a functionally equivalent synchronous implementation that can tolerate arbitrary communication latency between latches. By using latches we can break a long wire in short segments which can be traversed while meeting a single clock cycle constraint. The overall goal is to obtain a design that is robust with respect to delays of long wires, in a shorter time by reducing the multiple iterations between logical and physical design, and with performance that is optimized with respect to the speed of the single components of the design. We describe the details of the proposed methodology as well as report on the latency insensitive design of PDLX, an out-of-order microprocessor with speculative-execution. Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1999 | Noise analysis of non-autonomous radio frequency circuitsabstractConsiders the important problem of noise analysis of non-autonomous nonlinear RF circuits in the presence of input signal phase noise. We formulate this problem as a stochastic differential equation and solve it in the presence of circuit white-noise sources. We show that the output noise of a nonlinear non-autonomous circuit, driven by a periodic input signal with phase noise, is stationary-not cyclostationary (as would be predicted by traditional analyses). We also show that effect of the input signal phase noise is to act as additional white noise source. This result is derived using a full nonlinear analysis of the problem and cannot be predicted by traditional linear analysis-based techniques. Input signal phase noise can be an important portion of the overall output noise of the non-autonomous circuit. In our opinion, existing analyses have not considered this effect in a rigorous manner. We also relate this solution to results of the existing nonlinear time-domain and frequency-domain methods of noise analysis and point out the modifications required for the present techniques. We illustrate our technique using an example. Amit Mehrotra, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1999 | System Design: Traditional Concepts and New ParadigmsabstractRecent advances in system design are presented. The shift towards flexible hardware architectures that can support a variety of applications via programmability and reconfigurability is underlined. Essential to this process is the definition and use of platforms. We give a novel abstract, definition of platform and show its use in system design, drawing examples from the automotive system design field. Alberto Ferrari, Alberto L. Sangiovanni-Vincentelli |
ICCD | 2 |
| 1999 | Synthesis of software programs for embedded control applicationsabstractSoftware components for embedded reactive real-time applications must satisfy tight code size and run-time constraints. Cooperating finite state machines provide convenient intermediate format for embedded system co-synthesis, between high-level specification languages and software or hardware implementations. We propose a software generation methodology that takes advantage of a restricted class of specifications and allows for tight control over the implementation cost. The methodology exploits several techniques from the domain of Boolean function optimization. We also describe how the simplified control/data-flow graph used as an intermediate representation can be used to accurately estimate the size and timing cost of the final executable code. Felice Balarin, Massimiliano Chiodo, Paolo Giusto, Harry Hsieh, Attila Jurecska, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli, Ellen Sentovich, Kei Suzuki |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 7 |
| 1999 | Substrate optimization based on semi-analytical techniquesabstractSeveral methods are presented for highly efficient calculation of substrate noise transport in integrated circuits. A three-dimensional Green's function-based boundary element method, accelerated through use of the fast Fourier transform, allows the computation of sensitivities with respect to all substrate parameters at a considerably higher speed than any methods reported in the literature. Substrate sensitivities are used in a number of physical optimization tools, such as placement and trend analysis. The aim is a fast and accurate estimation of the impact of technology migration and/or layout redesign on substrate noise and, ultimately, on the circuit's overall performance. The suitability of the approach is shown through industrial-strength mixed-mode integrated circuits fabricated on a standard CMOS process. Edoardo Charbon, Ranjit Gharpurey, Robert G. Meyer, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1999 | Modeling digital substrate noise injection in mixed-signal IC'sabstractTechniques are presented to compactly represent substrate noise currents injected by digital networks. Using device-level simulation, every gate in a given library is modeled by means of the signal waveform it injects into the substrate, depending on its input transition scheme. For a given sequence of input vectors, the switching activity of every node in the Boolean network is computed. Assuming that technology mapping has been performed, each node corresponds to a gate in the library, hence, to a specific injection waveform. The noise contribution of each node is computed by convolving its switching activity with the associated injection waveforms. The total injected noise for the digital block is then obtained by summing all the noise contributions in the circuit. The resulting injected noise can be viewed as a random process, whose power spectrum is computed using standard signal processing techniques. A study was performed on a number of standard benchmark circuits to verify the validity of the assumptions and to measure the accuracy of the obtained power spectra. Edoardo Charbon, Paolo Miliozzi, Luca P. Carloni, Alberto Ferrari, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 5 |
| 1998 | A Case Study in Embedded System Design: An Engine Control UnitabstractA number of techniques and software tools for embedded system design have been recently proposed. However, the current practice in the designer community is heavily based on manual techniques and on past experience rather than on a rigorous approach to design. To advance the state of the art it is important to address a number of relevant design problems and solve them to demonstrate the power of the new approaches. Tullio Cuatto, Claudio Passerone, Luciano Lavagno, Attila Jurecska, Antonino Damiano, Claudio Sansoè, Alberto L. Sangiovanni-Vincentelli |
DAC | 7 |
| 1998 | Automatic Synthesis of Interfaces Between Incompatible ProtocolsabstractA t the system level, reusable Intellectual Property (or IP) blo cks can be represented abstractly as blocks that exchange messages. The concrete implementations of these IP blocks m ust exc hange the messages through complex signaling protocols. Interfacing bet ween IP that use different signaling protocols is a tedious and error prone design task. We propose using regular expression based protocol descriptions to sho w ho w to map the message on to a signaling protocol. Given t w o protocols,an algorithm is proposed to build an interface machine. We ha ve implemented our algorithm in a program named PIG that synthesizes a Verilog implementation based on a regular expression protocol description. Roberto Passerone, James A. Rowson, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1998 | An Exact Input Encoding Algorithm for BDDs Representing FSMsabstractWe address the problem of encoding the state variables of a finite state machine such that the BDD representing its characteristic function has the minimum number of nodes. We present an exact formulation of the problem. Our formulation characterizes the two BDD reduction rules by deriving conditions under which these reduction rules can be applied. We then provide an algorithm that finds these conditions and solves the problem by formulating it as a 2-CNF formula and extracting all its prime implicants. In addition to this, we implemented a simulated annealing algorithm for this problem and provide a thorough experiment of the impact of encoding on a BDD representing an FSM with different orderings. Wilsin Gosti, Alberto L. Sangiovanni-Vincentelli, Tiziano Villa, Alexander Saldanha |
Great Lakes Symposium on VLSI | 2 |
| 1998 | Wireplanning in logic synthesisabstracth this paper, we proWse a new logic synthesis methodology to deal with the increasing imprtance of the interconnect delay in deepsubmicron technologies.We first show that conventional logic synthesis techniques can produce circuits which wi~have long paths even if placed optimally.Then, we charactetie the conditions under which this cm happen and propose logic synthesis techniques which pmduw circuits which are "bettefl for placement.Our proposed approach still separates logic synthesis from physical design. Wilsin Gosti, Amit Narayan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1998 | The transistor: an invention becomes a big businessabstractWorldwide electronic equipment sales in 1996 were $851 billion, of which 16.5% or $140 billion were semiconductors. By the year 2000, estimates show that the semiconductor portion of equipment sales will grow to 21.1% or about $263 billion. This paper sets about to examine the birth and critical milestones of this phenomenal world-changing industry. Starting immediately after the Second World War, Bell Laboratories' management established a group to investigate semiconductors with a view to their application in telephone equipment. The group, headed by W. Shockley and including J. Bardeen and W. Brattain, was fully in place by January 1946. By December of the following year, Brattain and Bardeen had discovered the point-contact transistor. Early in the following year, Shockley established his theory of minority carrier injection and predicted the operation of the junction transistor. This paper outlines the growth of this business, starting initially among vacuum-tube manufacturers and spreading to high-growth-rate startups and on to major international companies. The importance of the U.S. military and space programs in the critical early days of both the transistor and the integrated circuit are touched on briefly. This paper gives careful attention to the birth and current state of the semiconductor scene of the Asian countries of Japan, Korea, and Taiwan. A review of the semiconductor industry in Europe, along with its decline and resurgence, is included. To complete the picture, the authors discuss the semiconductor industry decline and resurgence in the United States along with the contribution of SEMATECH and the importance of the personal computer to the U.S. recovery. This paper has two key appendixes. One focuses on the role of memory products as the industry enters the next century and the other complements the first by addressing the advent of system application-specific integrated circuits and the need for "continuous innovation" to meet the needs of each new product generation. These appendixes show the continuation of the semiconductor industry's traditional role in all electronic products namely, that of providing improved features, performance, and functionality with ever lower costs and higher quality. C. Mark Melliar-Smith, Michael G. Borrus, Douglas E. Haggan, Tyler Lowrey, Alberto L. Sangiovanni-Vincentelli, William W. Troutman |
Proc. IEEE | 5 |
| 1998 | Exact Minimization of Binary Decision Diagrams Using Implicit TechniquesabstractThis paper addresses the problem of binary decision diagram (BDD) minimization in the presence of don't care sets. Specifically given an incompletely specified function g and a fixed ordering of the variables, we propose an exact algorithm for selecting f such that f is a cover for g and the binary decision diagram for f is of minimum size. The approach described is the only known exact algorithm for this problem not based on the enumeration of the assignments to the points in the don't care set. We show also that our problem is NP-complete. We show that the BDD minimization problem can be formulated as a binate covering problem and solved using implicit enumeration techniques. In particular, we show that the minimum-sized binary decision diagram compatible with the specification can be found by solving a problem that is very similar to the problem of reducing incompletely specified finite state machines. We report experiments of an implicit implementation of our algorithm, by means of which a class of interesting examples was solved exactly. We compare it with existing heuristic algorithms to measure the quality of the latter. Arlindo L. Oliveira, Luca P. Carloni, Tiziano Villa, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Computers | 4 |
| 1998 | Theory and algorithms for face hypercube embeddingabstractWe present a new matrix formulation of the face hypercube embedding problem that motivates the design of an efficient search strategy to find an encoding that satisfies all faces of minimum length. Increasing dimensions of the Boolean space are explored; for a given dimension constraints are satisfied one at a time. The following features help to reduce the nodes of the solution space that must be explored: candidate cubes instead of candidate codes are generated, cubes yielding symmetric solutions are not generated, a smaller sufficient set of solutions (producing basic sections) is explored, necessary conditions help discard unsuitable candidate cubes, early detection that a partial solution cannot be extended to be a global solution prunes infeasible portions of the search tree. We have implemented a prototype package minimum input satisfaction kernel (MINSK) based on the previous ideas and run experiments to evaluate it. The experiments show that MINSK is faster and solves more problems than any available algorithm. Moreover, MINSK is a robust algorithm, while most of the proposed alternatives are not. Besides most problems of the complete Microelectronics Center of North Carolina (MCNC) benchmark suite, other solved examples include an important set of decoder programmable logic arrays (PLA's) coming from the design of microprocessor instruction sets. Eugene Goldberg, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1998 | A framework for comparing models of computationabstractWe give a denotational framework (a "meta model") within which certain properties of models of computation can be compared. It describes concurrent processes in general terms as sets of possible behaviors. A process is determinate if, given the constraints imposed by the inputs, there are exactly one or exactly zero behaviors. Compositions of processes are processes with behaviors in the intersection of the behaviors of the component processes. The interaction between processes is through signals, which are collections of events. Each event is a value-tag pair, where the tags can come from a partially ordered or totally ordered set. Timed models are where the set of tags is totally ordered. Synchronous events share the same tag, and synchronous signals contain events with the same set of tags. Synchronous processes have only synchronous signals as behaviors. Strict causality (in timed tag systems) and continuity (in untimed tag systems) ensure determinacy under certain technical conditions. The framework is used to compare certain essential features of various models of computation, including Kahn process networks, dataflow, sequential processes, concurrent sequential processes with rendezvous, Petri nets, and discrete-event systems. Edward A. Lee, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1998 | Modeling reactive systems in JavaabstractWe present an application of the Java TM programming language to specify and implement reactive real-time systems. We have developed and tested a collection of classes and methods to describe concurrent modules and their asynchronous communication by means of signals. The control structures are closely patterned after those of the synchronous language Esterel , succinctly describing concurrency, sequencing and preemption. We show the user-friendliness and efficiency of the proposed technique by using an example from the automotive domain. Claudio Passerone, Claudio Sansoè, Luciano Lavagno, Patrick C. McGeer, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli |
ACM Trans. Design Autom. Electr. Syst. | 7 |
| 1997 | Trade-off evaluation in embedded system design via co-simulationabstractCurrent design methodologies for embedded systems often force the designer to evaluate early in the design process architectural choices that will heavily impact the cost and performance of the final product. Examples of these choices are hardware/software partitioning, choice of the micro-controller, and choice of a run-time scheduling method. This paper describes how to help the designer in this task, by providing a flexible co-simulation environment in which these alternatives can be interactively evaluated. Claudio Passerone, Luciano Lavagno, Claudio Sansoè, Massimiliano Chiodo, Alberto L. Sangiovanni-Vincentelli |
ASP-DAC | 5 |
| 1997 | Schedule Validation for Embedded Reactive Real-Time SystemsabstractTask scheduling for reactive real time systems is adifficult problem due to tight constraints that theschedule must satisfy.A static priority schemeis proposed here that can be formally validated.The method is applicable both for preemptiveand non-preemptive schedules and is conservativein the sense that a valid schedule may bedeclared invalid, but no invalid schedule may bedeclared valid.Experimental results show thatthe run time of our validation method is negligiblewith respect to other steps in system designprocess, and compares favorably with othermethods of schedule validation. Felice Balarin, Alberto L. Sangiovanni-Vincentelli |
DAC | 2 |
| 1997 | Fast Hardware/Software Co-Simulation for Virtual Prototyping and Trade-Off AnalysisabstractHardware/Software co-simulation is generally performed with separate simulation models. This makes trade-off evaluation difficult, because the models must bere-compiled whenever some architectural choice is changed. We propose a technique to simulate hardware and software that is almost cycle accurate, and uses the same model for both types of components. Only the timing information used for synchronization needs to be changed to modify the processor choice, the implementation choice, or the scheduling policy. We show how this technique can be used to decide the implementation of a real-life example, a car dashboard controller. Claudio Passerone, Luciano Lavagno, Massimiliano Chiodo, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1997 | Interface-Based DesignabstractA new system design methodology is proposed that separates communicationfrom behavior. To demonstrate the methodology weapplied it to a simple ATM design. Since verification is clearly amajor stumbling block for large system design, we focussed on theverification aspects of our methodology.In particular, a simulator was developed that is based on the communicationparadigm typical of our methodology. The simulatorgives substantial performance improvements without sacrificinguser access to detail.Finally, the potential for this methodology to improve verification,modeling and synthesis is explored. James A. Rowson, Alberto L. Sangiovanni-Vincentelli |
DAC | 2 |
| 1997 | Logic synthesis for large pass transistor circuitsabstractPass transistor logic (PTL) can be a promising alternative to static CMOS for deep sub-micron design. The authors motivate the need for CAD algorithms for PTL circuit design and propose decomposed BDDs as a suitable logic level representation for synthesis of PTL networks. Decomposed BDDs can represent large, arbitrary functions as a multistage circuit and can exploit the natural, efficient mapping of a BDD to PTL. A comprehensive synthesis flow based on decomposed BDDs is outlined for PTL design. They show that the proposed approach allows one to make logic-level optimizations similar to the traditional multi-level network based synthesis flow for static CMOS, and also makes possible optimizations with a direct impact on area, delay and power of the final circuit implementation which do nor have any equivalent in the traditional approach. They also present a set of heuristical algorithms to synthesize PTL circuits optimized for area, delay and power which are key to the proposed synthesis flow. Experimental results on ISCAS benchmark circuits show that the technique yields PTL circuits with substantial improvements over static CMOS designs. In addition, to the best of their knowledge this is the first time PTL circuits have been synthesized for the entire ISCAS benchmark set. Premal Buch, Amit Narayan, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1997 | Trace driven logic synthesis - application to power minimizationabstractA trace driven methodology for logic synthesis and optimization is proposed. Given a logic description of a digital circuit C and an expected trace of input vectors T, an implementation of C that optimizes a cost function under application of T is derived. This approach is effective in capturing and utilizing the correlations that exist between input signals on an application specific design. The idea is novel since it proposes synthesis and optimization at the logic level where the goal is to optimize the average case rather than the worst case for a chosen cost metric. The paper focuses on the development of algorithms for trace driven optimization to minimize the switching power in multi level networks. The average net power reduction (internal plus I/O power) obtained on a set of benchmark FSMs is 14%, while the average reduction in internal power is 25%. We also demonstrate that the I/O transition activity provides an upper bound on the power reduction that can be achieved by combinational logic synthesis. Luca P. Carloni, Patrick C. McGeer, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1997 | Negative thinking by incremental problem solving: application to unate coveringabstractWe introduce a new technique to solve exactly a discrete optimization problem, based on the paradigm of "negative" thinking. The motivation is that when searching the space of solutions, often a good solution is reached quickly and then improved only a few times before the optimum is found: hence most of the solution space is explored to certify optimality, but it does not yield any improvement of the cost function. So it is quite natural for an algorithm to be "skeptical" about the chance to improve the current best solution. For illustration we have applied our approach to the unate covering problem. We designed a procedure, raiser, implementing a negative thinking search, which is incorporated into a common branch-and-bound procedure. Experiments show that our program, AURA, outperforms both ESPRESSO and our enhancement of ESPRESSO using Coudert's limit lower bound. It is always faster and in the most difficult examples either has a running time better by up to two orders of magnitude, or the other programs fail to finish due to timeout or spaceout. The package SCHERZO is faster on some examples and loses on others, due to a less powerful pruning strategy of the search space, partially mitigated by a more effective computation of the maximal independent set. Eugene Goldberg, Luca P. Carloni, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 5 |
| 1997 | A fast and robust exact algorithm for face embeddingabstractWe present a new matrix formulation of the face hypercube embedding problem that motivates the design of an efficient search strategy to find an encoding that satisfies all faces of minimum length. Increasing dimensions of the Boolean space are explored; for a given dimension constraints are satisfied one at a time. The following features help to reduce the nodes of the solution space that must be explored: candidate cubes instead of candidate codes are generated, cubes yielding symmetric solutions are not generated, a smaller sufficient set of solutions (producing basic sections) is explored, necessary conditions help discard unsuitable candidate cubes, early detection that a partial solution cannot be extended to be a global solution prunes infeasible portions of the search tree. We have implemented a prototype package MINSK based on the previous ideas and run experiments to evaluate it. The experiments show that MINSK is faster and solves more problems than any available algorithm. Moreover, MINSK is a robust algorithm, while most of the proposed alternatives are not. Besides most problems of the complete MCNC benchmark suite, other solved examples include an important set of decoder PLAs coming from the design of microprocessor instruction sets. Eugene Goldberg, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1997 | Sequential optimisation without state space explorationabstractWe propose an algorithm for area optimisation of sequential circuits through redundancy removal. The algorithm finds compatible redundancies by implying values over nets in the circuit. The potentially exponential cost of state space traversal is avoided and the redundancies found can all be removed at once. The optimised circuit is a safe delayed replacement of the original circuit. The algorithm computes a set of compatible sequential redundancies and simplifies the circuit by propagating them through the circuit. We demonstrate the efficacy of the algorithm even for large circuits through experimental results on benchmark circuits. Amit Mehrotra, Shaz Qadeer, Vigyan Singhal, Robert K. Brayton, Adnan Aziz, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 6 |
| 1997 | Reachability analysis using partitioned-ROBDDsabstractWe address the problem of finite state machine (FSM) traversal, a key step in most sequential verification and synthesis algorithms. We propose the use of partitioned ROBDDs to reduce the memory explosion problem associated with symbolic state space exploration techniques. In our technique, the reachable state set is represented as a partitioned ROBDD (A. Narayan et al., 1996). Different partitions of the Boolean space are allowed to have different variable orderings and only one partition needs to be in memory at any given time. We show the effectiveness of our approach on a set of ISCAS89 benchmark circuits. Our techniques result in a significant reduction in total memory utilization. For a given memory limit, partitioned ROBDD based method can complete traversal for many circuits for which monolithic ROBDDs fail. For circuits where both partitioned ROBDDs as well as monolithic ROBDDs cannot complete traversal, partitioned ROBDDs can reach a significantly larger set of states. Amit Narayan, Adrian J. Isles, Jawahar Jain, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 5 |
| 1997 | A Survey of Techniques for Formal Verification of Combinational CircuitsabstractWith the increase in the complexity of present day systems, proving the correctness of a design has become a major concern. Simulation based methodologies are generally inadequate to validate the correctness of a design with a reasonable confidence. More and more designers are moving towards formal methods to guarantee the correctness of their designs. The authors survey some state-of-the-art techniques used to perform automatic verification of combinational circuits. They classify the current approaches for combinational verification into two categories: functional and structural. The functional methods consist of representing a circuit as a canonical decision diagram. Two circuits are equivalent if and only if their decision diagrams are equal. The structural methods consist of identifying related nodes in the circuit and using them to simplify the problem of verification. They briefly describe some of the methods in both the categories and discuss their merits and drawbacks. Jawahar Jain, Amit Narayan, Alberto L. Sangiovanni-Vincentelli |
ICCD | 4 |
| 1997 | Dynamic Reordering in a Breadth-First Manipulation Based BDD Package: Challenges and SolutionsabstractThe breadth-first manipulation technique has proven effective in dealing with very large sized BDDs. However, until now the lack of dynamic variable reordering has remained an obstacle in its acceptance. The goal of the work is to provide efficient techniques to address this issue. After identifying the problems with implementing variable swapping (the core operation in dynamic reordering) in breadth-first based packages, the authors propose techniques to handle the computational and memory overheads. They feel that combining dynamic reordering with the powerful manipulation algorithms of a breadth-first based scheme can significantly enhance the performance of BDD based algorithms. The efficiency of the proposed techniques is demonstrated on a range of examples. Rajeev Ranjan 0001, Wilsin Gosti, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCD | 4 |
| 1997 | Design of embedded systems: formal models, validation, and synthesisabstractThis paper addresses the design of reactive real-time embedded systems. Such systems are often heterogeneous in implementation technologies and design styles, for example by combining hardware application-specific integrated circuits (ASICs) with embedded software. The concurrent design process for such embedded systems involves solving the specification, validation, and synthesis problems. We review the variety of approaches to these problems that have been taken. Stephen A. Edwards, Luciano Lavagno, Edward A. Lee, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 4 |
| 1997 | Implicit computation of compatible sets for state minimization of ISFSMsabstractThe computation of sets of compatibles of incompletely specified finite-state machines (ISFSMs) is a key step in sequential synthesis. This paper presents implicit computations to obtain sets of maximal compatibles, compatibles, prime compatibles, implied sets, and class sets. The computations are implemented by means of BDDs that realize the characteristic functions of these sets. We have demonstrated with experiments from a variety of benchmarks that implicit techniques allow us to handle examples exhibiting a number of compatibles up to 2/sup 1500/, an achievement outside the scope of programs based on explicit enumeration. We have shown, in practice, that ISFMSs with a very large number of compatibles may be produced as intermediate steps of logic synthesis algorithms, for instance, in the case of asynchronous synthesis. This shows that the proposed approach not only has a theoretical interest, but also practical relevance for current logic synthesis applications, as shown by its application to ISFSM state minimization. Timothy Kam, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1997 | Theory and algorithms for state minimization of nondeterministic FSMsabstractThis paper addresses state minimization problems of different classes of nondeterministic finite-state machines (NDFSMs). We describe a fully implicit algorithm for state minimization of pseudo nondeterministic FSM's (PNDFSMs). The results of our implementation are reported and shown to be superior to a previous explicit formulation. We could solve exactly all but one problem of a published benchmark, while an explicit program could complete approximately one half of the examples, and in those cases, with longer run times. Then we present a theoretical solution to the problem of exact state minimization of general NDFSMs, based on the proposal of generalized compatibles. This gives an algorithmic framework to explore behaviors contained in a general NDFSM. Timothy Kam, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1997 | Explicit and implicit algorithms for binate covering problemsabstractWe survey techniques for solving binate covering problems, an optimization step often occurring in logic synthesis applications. Standard exact solutions are found with a branch-and-bound exhaustive search, made more efficient by bounding away regions of the search space. Standard approaches are said to be explicit because they work on a direct representation of the binate table, usually as a matrix. Recently, covering problems involving large tables have been attacked with implicit techniques. They are based on the representation by reduced-ordered binary decision diagrams of an encoding of the binate table. We show how table reductions, computation of a lower bound, and of a branching column can be performed on the table so represented. We report experiments for two different applications that demonstrate that implicit techniques handle instances beyond the reach of explicit techniques. Various aspects of our original research are presented for the first time, together with a selection of the most important old and new results scattered in many sources. Tiziano Villa, Timothy Kam, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1997 | Symbolic two-level minimizationabstractIn this paper, we present a symbolic minimization procedure to obtain optimal two-level implementations of finite-state machines. Encoding based on symbolic minimization consists of optimizing the symbolic representation, and then transforming the optimized symbolic description into a compatible two-valued representation by satisfying encoding constraints (bitwise logic relations) imposed on the binary codes that replace the symbols. Our symbolic minimization procedure captures the sharing of product terms due to ORing effects in the output part of a two-level implementation of the symbolic cover. Face, dominance, and disjunctive constraints are generated. Product terms are accepted in a symbolic minimized cover only when they induce compatible encoding constraints. At the end, a set of codes that satisfy all constraints is computed. The quality of this synthesis procedure is shown by the fact that the cardinality of the cover obtained by symbolic minimization and of the cover obtained by replacing the codes in the initial cover and then minimizing it with ESPRESSO are very close. Experiments show that in some cases, our procedure improves on the best results of state-of-art tools. Tiziano Villa, Alexander Saldanha, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1996 | VIS: A System for Verification and Synthesis
Robert K. Brayton, Gary D. Hachtel, Alberto L. Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen A. Edwards, Sunil P. Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev Ranjan 0001, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa |
CAV | 3 |
| 1996 | Formal Verification of Embedded Systems based on CFSM NetworksabstractBoth timing and functional properties are essential to characterize the correct behavior of an embedded system.Verication is in general performed either by simulation, or by bread-boarding.Given the safety requirements of such systems, a formal proof that the properties are indeed satised is highly desirable.In this paper, we present a formal veri cation methodology for embedded systems.The formal model for the behavior of the system used in POLIS is a network of Codesign Finite State Machines.This model is translated into automata, and veri ed using automatatheoretic techniques.An industrial embedded system is veri ed using the methodology.W e demonstrate that abstractions and separation of timing and functionality is crucial for the successful use of formal veri cation for this example.We also show that in POLIS abstractions and separation of timing and functionality can be done by simple syntactic modi cation of the representation of the system. Felice Balarin, Harry Hsieh, Attila Jurecska, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
DAC | 5 |
| 1996 | Engineering Change in a Non-Deterministic FSM Settingabstractpersonal or class-room use is granted without fee provided that copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication and its date appear, and notice is given that copying is Sunil P. Khatri, Amit Narayan, Sriram C. Krishnan, Kenneth L. McMillan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 6 |
| 1996 | Use of Sensitivities and Generalized Substrate Models in Mixed-Signal IC DesignabstractA novel methodology for circuit design and automatic layout generation is proposed for a class of mixed-signal circuits in presence of layout parasitics and substrate induced noise.Accurate and efficient evaluation of the circuit during design is possible by taking into account such non-idealities.Techniques are presented to derive and use a set of constraints on substrate noise and on the geometric instances of the layout.Verification is performed using substrate extraction in combination with parasitic estimation techniques.To show the suitability of the approach, a VCO for a PLL has been designed and implemented in a CMOS 1m technology.The circuit has been optimized both at the schematic and at the layout level for power and performance, while its sensitivity to layout parasitics and substrate noise has been minimized. Paolo Miliozzi, Iasson Vassiliou, Edoardo Charbon, Enrico Malavasi, Alberto L. Sangiovanni-Vincentelli |
DAC | 5 |
| 1996 | High Performance BDD Package By Exploiting Memory HiercharchyabstractThe success of binary decision diagram (BDD) based algorithms for verification depend on the availability of a high performance package to manipulate very large BDDs. State-of-the-art BDD packages, based on the conventional depth-first technique, limit the size of the BDDs due to a disorderlymemory accesspatterns that results in unacceptably high elapsed time when the BDD size exceeds the main memory capacity. We present a high performance BDD package that enables manipulation of very large BDDs by using an iterative breadth-first technique directed towards localizing the memory accesses to exploit the memory system hierarchy. The new memory-oriented performance features of this package are 1) an architecture independent customized memory management scheme, 2) the ability to issue multiple independent BDD operations (superscalarity) , and 3) the ability to perform multiple BDD operations even when the operands of some BDD operations are the result of some other operations yet to be com... Jagesh V. Sanghavi, Rajeev Ranjan 0001, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1996 | Verification of Electronic Systemsabstraction, which eliminates details that are of no importance when checking whether a design satisfies a particular property. ffl Decomposition, which consists of breaking the design at a given level of the hierarchy into components that can be designed and verified almost independently. These mechanisms can be applied to different classes of designs: from embedded controllers to computers, from microprocessors to digital-to-analog converters. They are not only useful in the verification process but also in the design process per se making verification itself unnecessary in some cases. For example, formalization of the design specifications is required for formal verification but it also helps in design transfer between different organizations eliminating the risk of losing knowledge about the design and its specifications, thus making verification before and after the transfer unnecessary. We argue that almost all advances in verification stem from the application of these three basic con... Alberto L. Sangiovanni-Vincentelli, Patrick C. McGeer, Alexander Saldanha |
DAC | 1 |
| 1996 | Efficient Software Performance Estimation Methods for Hardware/Software CodesignabstractThe performance estimation of a target system at a higher level of abstraction is very important in hardware/software codesign. We focus on software performance estimation, including both the execution time and the code size. We present two estimation methods at different levels of abstraction for use in the POLIS hardware/software codesign system. The experimental results show that the accuracy of our methods is usually within /spl plusmn/20%. Kei Suzuki, Alberto L. Sangiovanni-Vincentelli |
DAC | 2 |
| 1996 | VIS
Robert K. Brayton, Gary D. Hachtel, Alberto L. Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen A. Edwards, Sunil P. Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev Ranjan 0001, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa |
FMCAD | 3 |
| 1996 | Decomposition Techniques for Efficient ROBDD Construction
Jawahar Jain, Amit Narayan, C. Coelho 0001, Sunil P. Khatri, Alberto L. Sangiovanni-Vincentelli, Robert K. Brayton |
FMCAD | 5 |
| 1996 | Compact and complete test set generation for multiple stuck-faultsabstractWe propose a novel procedure for testing all multiple stuck-faults in a logic circuit using two complementary algorithms. The first algorithm finds pairs of input vectors to detect the occurrence of target single stuck-faults independent of the occurrence of other faults. The second uses a sophisticated branch and bound procedure to complete the test set generation on the faults undetected by the first algorithm. The technique is complete and applies to all circuits. Experimental results presented in this paper demonstrate that compact and complete test sets can be quickly generated for standard benchmark circuits. Alok Agrawal, Alexander Saldanha, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1996 | Semi-analytical techniques for substrate characterization in the design of mixed-signal ICsabstractA number of methods are presented for highly efficient calculation of substrate current transport. A three-dimensional Green's Function based substrate representation, in combination with the use of the Fast Fourier Transform, significantly speeds up the computation of sensitivities with respect to all parameters associated with a given architecture. Substrate sensitivity analysis is used in a number of physical optimization tools, such as placement and trend analysis for the estimation of the impact of technology migration and/or layout re-design. Edoardo Charbon, Ranjit Gharpurey, Alberto L. Sangiovanni-Vincentelli, Robert G. Meyer |
ICCAD | 3 |
| 1996 | Generalized constraint generation in the presence of non-deterministic parasiticsabstractIn a constraint-driven layout synthesis environment, parasitic constraints are generated and implemented in each phase of the design process to meet a given set of performance specifications. The success of the synthesis phase depends in great part on the effectiveness and the generality of the constraint generation process. None of the existing approaches to the constraint generation problem however are suitable for a number of parasitic effects in active and passive devices due to non-deterministic process variations. To address this problem a novel methodology is proposed based on the separation of all variables associated with non-deterministic parasitics, thus allowing the translation of the problem into an equivalent one in which conventional constrained optimization techniques can be used. The requirements, of the method are a well-defined set of statistical properties for all parasitics and a reasonable degree of linearity of the performance measures relevant to design. Edoardo Charbon, Paolo Miliozzi, Enrico Malavasi, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1996 | Hierarchical statistical characterization of mixed-signal circuits using behavioral modelingabstractA methodology for hierarchical statistical circuit characterization which does not rely upon circuit-level Monte Carlo simulation is presented. The methodology uses principal component analysis, response surface methodology, and statistics to directly calculate the statistical distributions of higher-level parameters from the distributions of lower-level parameters. We have used the methodology to characterize a folded cascode operational amplifier and a phase-locked loop. This methodology permits the statistical characterization of large analog and mixed-signal systems, many of which are extremely time-consuming or impossible to characterize using existing methods. Eric Felt, Stefano Zanella, Carlo Guardiani, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1996 | Digital sensitivity: predicting signal interaction using functional analysisabstractMaintaining signal integrity in digital systems is becoming increasingly difficult due to the rising number of analog effects seen in deep submicron design. One such effect, the signal crosstalk problem, is now a serious design concern. Signals which couple electrically may not affect system behavior because of timing or function in the digital domain. If we can isolate observable coupling then we can constrain layout synthesis to eliminate them. In this paper, we find that it is possible to predict signal interaction by signal functionality alone, leading to a significant amount of robust switching isolation, independent of parasitics introduced by layout or semiconductor process. We introduce techniques to predict signal interaction using functional sensitivity analysis. In general sequential networks we find that significant switching isolation can be extracted with efficient sensitivity analysis algorithms, thus giving promise to the goal of synthesizing layout free from crosstalk effects. Desmond Kirkpatrick, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1996 | Comparing models of computationabstractWe give a denotational framework (a meta model) within which certain properties of models of computation can be understood and compared. It describes concurrent processes as sets of possible behaviors. Compositions of processes are given as intersections of their behaviors. The interaction between processes is through signals, which are collections of events. Each event is a value-tag pair, where the tags can come from a partially ordered or totally ordered set. Timed models are where the set of tags is totally ordered. Synchronous events share the same tag, and synchronous signals contain events with the same set of tags. Synchronous systems contain synchronous signals. Strict causality (in timed systems) and continuity (in untimed systems) ensure determinacy under certain technical conditions. The framework is used to compare certain essential features of various models of computation, including Kahn process networks, dataflow, sequential processes, concurrent sequential processes with rendezvous, Petri nets, and discrete-event systems. Edward A. Lee, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1996 | Partitioned ROBDDs - a compact, canonical and efficiently manipulable representation for Boolean functionsabstractWe present a new representation for Boolean functions called Partitioned ROBDDs. In this representation we divide the Boolean space into 'k' partitions and represent a function over each partition as a separate ROBDD. We show that partitioned-ROBDDs are canonical and can be efficiently manipulated. Further they can be exponentially more compact than monolithic ROBDDs and even free BDDs. Moreover, at any given time, only one partition needs to be manipulated which further increases the space efficiency. In addition to showing the utility of partitioned-ROBDDs on special classes of functions, we provide automatic techniques for their construction. We show that for large circuits our techniques are more efficient in space as well as time over monolithic ROBDDs. Using these techniques, some complex industrial circuits could be verified for the first time. Amit Narayan, Jawahar Jain, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1996 | A video driver system designed using a top-down, constraint-driven methodologyabstractTo accelerate the design cycle for analog and mixed-signal systems, we have proposed a top-down, constraint-driven design methodology. The key idea of the proposed methodology is hierarchically propagating constraints from performance specifications to layout. Consequently, it is essential to provide the necessary tools and techniques enabling the efficient constraint propagation. To illustrate the applicability of the proposed methodology to the design of larger systems, we present in this paper the complete design flow for a video driver system. Critical advantages of the methodology illustrated with this design example include avoiding costly low level re-designs and getting working silicon parts from the first run. Following our approach, a jitter constraint is imposed at the system level and then is propagated hierarchically to the circuit blocks and layout, using behavioral modeling and simulation. Experimental results are presented from working fabricated parts. Iasson Vassiliou, Henry Chang, Alper Demir 0001, Edoardo Charbon, Paolo Miliozzi, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 6 |
| 1996 | Binary decision diagrams on network of workstationabstractThe success of all binary decision diagram (BDD) based synthesis and verification algorithms depend on the ability to efficiently manipulate very large BDDs. We present algorithms for manipulation of very large Binary Decision Diagrams (BDDs) on a network of workstations (NOW). A NOW provides a collection of main memories and disks which can be used effectively to create and manipulate very large BDDs. To make efficient use of memory resources of a Now, while completing execution in a reasonable amount of wall clock time, extension of breadth-first technique is used to manipulate BDDs. BDDs are partitioned such that nodes for a set of consecutive variables are assigned to the same workstation. We present experimental results to demonstrate the capability of such an approach and point towards the potential impact for manipulating very large BDDs. Rajeev Ranjan 0001, Jagesh V. Sanghavi, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCD | 4 |
| 1996 | Rapid-Prototyping of Embedded Systems via Reprogrammable DevicesabstractThis paper describes a flexible board-level rapid-prototyping environment for embedded control applications. The environment is based on an APTIX board populated by Xilinx FPGA devices, a 68hcll emulator, and APTIX programmable interconnect devices. Given a design consisting of logic and of software running on a micro-controller that implement a set of tasks, the prototype is obtained by programming the FPGA devices, the micro-controller emulator and the APTIX devices. This environment being based on programmable devices offers the flexibility to perform engineering changes, the performance needed to validate complex systems and the hardware set up for field tests. The key point in our approach is the use of results of our previous research on software and hardware synthesis as well as on some commercial tools to provide the designer with fast programming data from a high level description of the algorithms to be implemented. We demonstrate the effectiveness of the approach by showing a close-to real-life example from the automotive world. Stefano Cardelli, Massimiliano Chiodo, Paolo Giusto, Attila Jurecska, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
RSP | 6 |
| 1996 | Optimization of analog IC test structuresabstractA methodology for designing optimal analog integrated circuit test structures is presented. An optimal test structure is a circuit which allows one to characterize a specified set of circuit parameters as accurately as possible in the presence of measurement noise and other potential errors. The methodology is based upon recently developed statistical techniques for optimal design of experiments; these techniques allow analog systems to be characterized as accurately and efficiently as possible, thereby reducing cost and/or increasing accuracy. The usefulness of the methodology is illustrated with a fabricated circuit. The most interesting result is that relatively complex circuits are frequently more efficient than commonly used simple circuits. Eric Felt, Alberto L. Sangiovanni-Vincentelli |
VTS | 2 |
| 1996 | A Unified Signal Transition Graph Model for Asynchronous Control Circuit Synthesis
Alexandre Yakovlev, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
Formal Methods Syst. Des. | 3 |
| 1996 | Using the Minimum Description Length Principle to Infer Reduced Ordered Decision Graphs
Arlindo L. Oliveira, Alberto L. Sangiovanni-Vincentelli |
Mach. Learn. | 2 |
| 1996 | Time-domain non-Monte Carlo noise simulation for nonlinear dynamic circuits with arbitrary excitationsabstractA time-domain, non-Monte Carlo method for computer simulation of electrical noise in nonlinear dynamic circuits with arbitrary excitations and arbitrary large-signal waveforms is presented. This time-domain noise simulation method is based on results from the theory of stochastic differential equations. The noise simulation method is general in the following sense. Any nonlinear dynamic circuit with any kind of excitation, which can be simulated by the transient analysis routine in a circuit simulator, can be simulated by our noise simulator in time-domain to produce the noise variances and covariances of circuit variables as a function of time, provided that noise models for the devices in the circuit are available. Noise correlations between circuit variables at different time points can also be calculated. Previous work on computer simulation of noise in electronic circuits is reviewed with comparisons to our method. Shot, thermal, and flicker noise models for integrated-circuit devices, in the context of our time-domain noise simulation method, are discussed. The implementation of this noise simulation method in a circuit simulator (SPICE) is described. Two examples of noise simulation (a CMOS inverter and a BJT active mixer) are given. Alper Demir 0001, Edward W. Y. Liu, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1996 | Valid clock frequencies and their computation in wavepipelined circuitsabstractIt is known that wavepipelined circuits offer high performance, because their maximum clock frequencies are limited only by the path delay differences of the circuits, as opposed to the longest path delays. For proper operation, precision in clock frequency is essential. Using a new representation, Timed Boolean Functions, we derive analytical expressions for valid clocking intervals in terms of topological, 2-vector, and single vector delays, both the longest and the shortest. These intervals take into account both circuit functionality and timing characteristics, thus eliminating the pessimism caused by long and short false paths, and include effects of circuit parameters such as delay variations, clock skews, and setup and hold times of flip flops. In addition, we show that these intervals subsume Cotten's lower bound on valid clock period. Further, we study the problem of computing all enact valid clocking intervals and its computational complexity by demonstrating discontinuity and nonmonotonicity of the harmonic number H(/spl tau/) (the number of valid simultaneous data waves allowed) as a function of the clock period /spl tau/. Finally, we propose algorithms to compute the exact valid intervals for a given set of harmonic numbers and demonstrate performance enhancement of balanced circuits from ISCAS benchmarks with gate delay variations. William K. C. Lam, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1996 | Automation of IC layout with analog constraintsabstractA methodology for the automatic synthesis of full-custom IC layout with analog constraints is presented. The methodology guarantees that all performance constraints are met when feasible, or otherwise, infeasibility is detected as soon as possible, thus providing a robust and efficient design environment. In the proposed approach, performance specifications are translated into lower-level bounds on parasitics or geometric parameters, using sensitivity analysis. Bounds can be used by a set of specialized layout tools performing stack generation, placement, routing, and compaction. For each tool, a detailed description is provided of its functionality, of the way constraints are mapped and enforced, and of its impact on the design flow. Examples drawn from industrial applications are reported to illustrate the effectiveness of the approach. Enrico Malavasi, Edoardo Charbon, Eric Felt, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1996 | Combinational test generation using satisfiabilityabstractWe present a robust, efficient algorithm for combinational test generation using a reduction to satisfiability (SAT). The algorithm, Test Generation Using Satisfiability (TEGUS), solves a simplified test set characteristic equation using straightforward but powerful greedy heuristics, ordering the variables using depth-first search and selecting a variable from the next unsatisfied clause at each branching point. For difficult faults, the computation of global implications is iterated, which finds more implications than previous approaches and subsumes structural heuristics such as unique sensitization. Without random tests or fault simulation, TEGUS completes on every fault in the ISCAS networks, demonstrating its robustness, and is ten times faster for those networks which have been completed by previous algorithms. Our implementation of TEGUS can be used as a base line for comparing test generation algorithms; we present comparisons with 45 recently published algorithms. TEGUS combines the advantages of the elegant organization of SAT-based algorithms with the efficiency of structural algorithms. Paul R. Stephan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1995 | Synthesis of Software Programs for Embedded Control ApplicationsabstractArticle Free Access Share on Synthesis of software programs for embedded control application Authors: Massimiliano Chiodo Magneti Marelli, Italy Magneti Marelli, ItalyView Profile , Paolo Guisto Magneti Marelli, Italy Magneti Marelli, ItalyView Profile , Attila Jurecska Magneti Marelli, Italy Magneti Marelli, ItalyView Profile , Luciano Lavagno Dipartimento di Elettronica, Politecnico di Torino, Italy Dipartimento di Elettronica, Politecnico di Torino, ItalyView Profile , Ellen Sentovich Cadence Berkeley Labs, Berkeley, CA Cadence Berkeley Labs, Berkeley, CAView Profile , Harry Hsieh Department of EECS, Univ. of California, Berkeley, CA Department of EECS, Univ. of California, Berkeley, CAView Profile , Kei Suzuki Department of EECS, Univ. of California, Berkeley, CA Department of EECS, Univ. of California, Berkeley, CAView Profile , Alberto Sangiovanni-Vincentelli Department of EECS, Univ. of California, Berkeley, CA Department of EECS, Univ. of California, Berkeley, CAView Profile Authors Info & Claims DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation ConferenceJanuary 1995 Pages 587–592https://doi.org/10.1145/217474.217594Published:01 January 1995Publication History 36citation320DownloadsMetricsTotal Citations36Total Downloads320Last 12 Months5Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF Massimiliano Chiodo, Paolo Giusto, Attila Jurecska, Luciano Lavagno, Harry Hsieh, Kei Suzuki, Alberto L. Sangiovanni-Vincentelli, Ellen Sentovich |
DAC | 7 |
| 1995 | Timed Shannon Circuits: A Power-Efficient Design Style and Synthesis ToolabstractArticle Timed shared circuits: a power-efficient design style and synthesis tool Share on Authors: Luciano Lavagno Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CA Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CAView Profile , Patrick C. McGeer Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CA Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CAView Profile , Alexander Saldanha Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CA Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CAView Profile , Alberto L. Sangiovanni-Vincentelli Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CA Cadence Berkeley Laboratories, 1919 Addison Street, Suite 301, Berkeley-CAView Profile Authors Info & Claims DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation ConferenceJanuary 1995 Pages 254–260https://doi.org/10.1145/217474.217538Online:01 January 1995Publication History 21citation231DownloadsMetricsTotal Citations21Total Downloads231Last 12 Months1Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access Luciano Lavagno, Patrick C. McGeer, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1995 | Sequential synthesis using S1SabstractWe present a mathematical framework for analyzing the synthesis of interacting, finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in sequential synthesis. We obtain exact and approximate sets of permissible FSM network behavior, and address the issue of FSM realizability. This approach is also applied to synthesizing systems with fairness and timed systems. Adnan Aziz, Felice Balarin, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1995 | Fast discrete function evaluation using decision diagramsabstractAn approach for fast discrete function evaluation based on multi-valued decision diagrams (MDD) is proposed. The MDD for a logic function is translated into a table on, which function evaluation is performed by a sequence of address lookups. The value of a function for a given input assignment is obtained with at most one lookup per input. The main application is to cycle-based logic simulation of digital circuits, where the principal difference from other logic simulators is that only values of the output and latch ports are computed. Theoretically, decision-diagram based function evaluation offers orders-of-magnitude potential speedup over traditional logic simulation methods. In practice, memory bandwidth becomes the dominant consideration on large designs. We describe techniques to optimize usage of the memory hierarchy. Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia |
ICCAD | 4 |
| 1995 | Implicit state minimization of non-deterministic FSMsabstractThis paper addresses state minimization problems of different classes of non-deterministic finite state machines (NDFSMs). We present a theoretical solution to the problem of exact state minimization of general NDFSMs, based on the proposal of generalized compatibles. This gives an algorithmic frame to explore behaviors contained in a general NDFSM. Then we describe a fully implicit algorithm for state minimization of pseudo non-deterministic FSMs (PNDFSMs). The results of our implementation are reported and shown to be superior to a previous explicit formulation. We could solve exactly all but one problem of a published benchmark, while an explicit program could complete approximately one half of the examples, and in those cases with longer run times. Timothy Kam, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCD | 4 |
| 1995 | Inferring Reduced Ordered Decision Graphs of Minimum Description Length
Arlindo L. Oliveira, Alberto L. Sangiovanni-Vincentelli |
ICML | 2 |
| 1995 | An Iterative Approach to Verification of Real-Time Systems
Felice Balarin, Alberto L. Sangiovanni-Vincentelli |
Formal Methods Syst. Des. | 2 |
| 1995 | Automatic generation of analytical models for interconnect capacitancesabstractAn analytical-model generator for interconnect capacitances is presented. It obtains analytical expressions of self and coupling capacitances of interconnects for commonly encountered configurations, based on a series of numerical simulations and a partial knowledge of the flux components associated with the configurations. The configurations which are currently considered by this model generator are: (a) single line; (b) crossing lines; (c) parallel lines on the same layer; and (d) parallel lines on different layers (both overlapping and nonoverlapping).> Umakanta Choudhury, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1995 | Synthesis for testability techniques for asynchronous circuitsabstractOur goal is to synthesize hazard-free asynchronous circuits that are testable in the very stringent hazard-free robust path-delay-fault model. From a synthesis perspective producing circuits satisfying two very stringent requirements, namely, hazard-free operation and hazard-free robust path-delay-fault-testability, poses an especially exciting challenge. Here we present techniques which guarantee both hazard-free operation and hazard-free robust path-delay-fault testability, at the expense of possibly adding test inputs. We also give a set of heuristics which can improve hazard-free robust path-delay-fault testability without requiring such inputs. Finally, we present a procedure that guarantees testability in the less stringent robust gate-delay-fault model. Kurt Keutzer, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1995 | Delay fault coverage, test set size, and performance trade-offsabstractThe main disadvantage of the path delay fault model is that to achieve 100% testability every path must be tested. Since the number of paths is usually exponential in circuit size, this implies very large test sets for most circuits. Not surprisingly, all known analysis and synthesis techniques for 100% path delay fault testability are computationally infeasible on large circuits. We prove that 100% delay fault testability is not necessary to guarantee the speed of a combinational circuit. There exist path delay faults which can never impact the circuit delay (computed using any correct timing analysis method) unless some other path delay faults also affect it. These are termed robust dependent delay faults and need not be considered in delay fault testing. Necessary and sufficient conditions under which a set of path delay faults is robust dependent are proved; this yields more accurate and increased delay fault coverage estimates than previously used. Next, assuming only the existence of robust delay fault tests for a very small set of paths, we show how the circuit speed (clock period) can be selected such that 100% robust delay fault coverage is achieved. This leads to a quantitative tradeoff between the testing effort (measured by the size of the test set) for a circuit and the verifiability of its performance. Finally, under a bounded delay model, we show that the test set size can be reduced while maintaining the delay fault coverage for the specified circuit speed. Examples and experimental results are given to show the effect of these three techniques on the amount of delay fault testing necessary to guarantee correct operation.> William K. C. Lam, Alexander Saldanha, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1995 | Synthesis of hazard-free asynchronous circuits with bounded wire delaysabstractThis paper introduces a new synthesis methodology for asynchronous sequential control circuits from a high level specification, the signal transition graph (STG). The methodology is guaranteed to generate hazard-free circuits with the bounded wire-delay model, if the STG is live and has the complete state coding property. The methodology exploits knowledge of the environmental delays, speed-independence with respect to externally visible signals, and logic synthesis techniques. A proof that STG persistency is neither necessary nor sufficient for hazard-free implementation is given.> Luciano Lavagno, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1995 | An efficient heuristic procedure for solving the state assignment problem for event-based specificationsabstractWe propose a novel framework to solve the state assignment problem arising from the signal transition graph (STG) representation of an asynchronous circuit. We first establish a relation between STG's and finite state machines (FSM's). Then we solve the STG state assignment problem by minimizing the number of states in the corresponding FSM and by using a critical race-free state assignment technique. State signal transitions may be added to the original STG. A lower bound on the number of signals necessary to implement the STG is given. Our technique significantly increases the STG applicability as a specification for asynchronous circuits.> Luciano Lavagno, Cho W. Moon, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1995 | Verification of Nyquist data converters using behavioral simulationabstractA behavioral representation of Nyquist data converters is presented. The representation captures the static behavior of a memoryless Nyquist data converter including statistical variations. The variations are classified into noise and process variations according to how these nonidealities affect the converter behavior. To describe noise effects, a joint probability density function is used. To describe behavioral effects due to process variations, a Gaussian model is used. Using the behavioral representation, a novel strategy to calculate system performance is developed. The performance specifications of a converter, including offset error, full scale gain error, integral nonlinearity, differential nonlinearity, harmonic distortion, and signal-to-noise ratio, are calculated in two steps. First, the converter model parameters are extracted from the circuit. Then, the converter performance is computed using only the model parameters since the model captures the converter behavior. Experimental results agree well with SPICE simulations and confirm the validity of the model.> Edward W. Y. Liu, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1994 | On the Automatic Computation of Network Invariants
Felice Balarin, Alberto L. Sangiovanni-Vincentelli |
CAV | 2 |
| 1994 | HSIS: A BDD-Based Environment for Formal VerificationabstractArticle Free Access Share on HSIS: a BDD-based environment for formal verification Authors: A. Aziz Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , F. Balarin Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S.-T. Cheng Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. Hojati Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. Kam Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. C. Krishnan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Ranjan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. R. Shiple Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , V. Singhal Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. Tasiran Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , H.-Y. Wang Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Brayton Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , A. L. Sangiovanni-Vincentelli Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile Authors Info & Claims DAC '94: Proceedings of the 31st annual Design Automation ConferenceJune 1994 Pages 454–459https://doi.org/10.1145/196244.196467Published:06 June 1994Publication History 39citation325DownloadsMetricsTotal Citations39Total Downloads325Last 12 Months36Last 6 weeks17 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF Adnan Aziz, Felice Balarin, Szu-Tsung Cheng, Ramin Hojati, Timothy Kam, Sriram C. Krishnan, Rajeev Ranjan 0001, Thomas R. Shiple, Vigyan Singhal, Serdar Tasiran, Huey-Yih Wang, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 13 |
| 1994 | Chain Closure: A Problem in Molecular CADabstractConformational analysis is the problem of nding all minimal energy three-dimensional con gurations of molecules.Cyclic structures are of particular interest.An ecient algorithm based on a purely geometric approach that generates feasible con gurations very eciently is presented thus making full conformational analysis possible even for fairly large cyclic structures. Maria Domenica Di Benedetto, Pasquale Lucibello, Alberto L. Sangiovanni-Vincentelli, Ken Yamaguchi |
DAC | 3 |
| 1994 | Simultaneous Placement and Module Optimization of Analog IC'sabstractNew placement techniques are presented which substantially improve the process of automatic layout generation of analog IC's. Extremely tight specifications can be enforced on high-performance analog circuits by using simultaneous placement and module optimization. An algorithmic approach to module generation provides alternative sets of modules optimized with respect to area and performance but equivalent in terms of parasitics and topology. The final module selection is performed during the placement phase, based on Simulated Annealing. The flexibility of the annealing algorithm has been significantly improved, thus making it possible to more efficiently exploit the tradeoffs between area, parasitics and matching. Edoardo Charbon, Enrico Malavasi, Davide Pandini, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1994 | Panel: Complex System Verification: The Challenge AheadabstractNo abstract available. Ronald Collett, Mike Gianfagna, Michel Courtoy, Martin Baynes, Johan Van Ginderdeuren, Kenneth L. McMillan, Stephen Ricca, Alberto L. Sangiovanni-Vincentelli, Steve Sapiro, Naeem Zafar |
DAC | 8 |
| 1994 | A Fully Implicit Algorithm for Exact State MinimizationabstractImplicit computations of the solution set of optimization problems arising in logic synthesis hold the promise of enlarging the size of instances that can be solved exactly. The state minimization problem for incompletely specified machines is an important step for sequential circuit optimization. The problem is NP-hard. An exact algorithm consists of two steps: generation of sets of compatibles, and solution of a binate covering problem. This paper presents an implicit algorithm for exact state minimization of FSM's. There are various applications of logic synthesis that generate FSM's beyond the reach of state-of-art state minimization tools. Therefore it is of practical importance to revisit exact state minimization of ISFSM's and address the issue of representing implicitly the solution space. In this paper we show how to compute sets of maximal compatibles, compatibles and prime compatibles with implicit techniques and demonstrate that in this way it is possible to handle examples exhibiting a number of compatibles up to 21200, a number outside the scope of programs based on explicit enumeration [13]. We indicate also where such examples arise in practice. Then we address the final step of an implicit exact state minimization procedure, i.e. solving a binate table covering problem [24]. We present the first published algorithm for fully implicit exact binate covering. We report preliminary results of a prototype implementation capable of reducing huge binate tables (up to 106 rows and column)s and of carrying on the branch-and-bound procedure on an implicit representation of the table. Exact solutions to problems beyond the reach of traditional tools are so found Timothy Kam, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1994 | Exact Minimum Cycle Times for Finite State MachinesabstractIn current research, the minimum cycle times of finite state machines are estimated by computing the delays of the combinational logic in the finite state machines. Even though these methods deal with false paths, they ignore the sequential and periodic nature of minimum cycle times, and hence may give pessimistic results. In this paper, we first prove conditions under which combinational delays are correct upper bounds on minimum cycle times. Then, we present a sequential approach to compute the minimum cycle times of finite state machines, taking into account the effects of gate delay variations, reachable state space, initial states, unrealizable transitions, multiple cycle false paths, and periodicity of the present state vector sequences. We formulate and solve the problem exactly using Timed Boolean Functions, and give an efficient algorithm to solve for upper bounds of minimum cycle times. The exact formulation with Timed Boolean Functions provides a framework for further improvements on existing algorithms to compute the minimum cycle times. We implemented the algorithm and obtained the tightest bounds known on ISCAS benchmarks. From the experiments, we found that for about 20 % of the circuits (not all shown in section 8), combinational delays, e.g. floating, viability, and transition delays, give pessimistic upper bounds for cycle times by as much as 25%. 1 William K. C. Lam, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1994 | DA Algorithms in Non-EDA Applications: How Universal Are Our Techniques? (Panel)abstractNo abstract available. Patrick C. McGeer, Steven Trimberger, Erik Carlson, Dave Hightower, Ulrich Lauther, Alberto L. Sangiovanni-Vincentelli |
DAC | 6 |
| 1994 | Optimum Functional Decomposition Using EncodingabstractIn this paper, we revisit the classical problem of functional decomposition [1, 2] that arises so often in logic synthesis.One basic problem that has remained largely unaddressed to the best of our knowledge is that of decomposing a function such that the resulting sub-functions are simple, i.e., have small numberof cubes or literals.In this paper, we show h o w to solve this problem optimally.W e show that the problem is intimately related to the encoding problem, which is also of fundamental importance in sequential synthesis, especially state-machine synthesis.We formulate the optimum decomposition problem using encoding.In general, an input-output encoding formulation has to be employed.However, for eld-programmable gate array architectures that use look-up tables, the input encoding formulation suces, provided we use minimum-length codes.The last condition is really not a constraint, since each extra code bit means that an extra table has to be used (and that could be expensive).The unused codes are used as don't cares for simplifying the sub-functions.We compare the original implementation of functional decomposition, which ignores the encoding problem, with the new version that uses encoding while doing decomposition.We obtain an average improvement o f o v er 20% on a set of standard benchmarks for look-up table architectures. Rajeev Murgai, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1994 | Performance Optimization Using Exact SensitizationabstractA common approach to performance optimization of circuits focuses on re-synthesis to reduce the length of all paths greater than the desired delay .We describe a new delay optimization procedure that optimizes only sensitizable paths greater than .Unlike previous methods that use topological analysis only, this method accounts for both functional and topological interactions in the circuit.Comprehensive experimental results comparing the proposed technique to a state-of-the-art performance optimization procedure are presented for combinational and sequential logic circuits. Alexander Saldanha, Heather Harkness, Patrick C. McGeer, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 5 |
| 1994 | Heuristic Minimization of BDDs Using Don't CaresabstractWe present heuristic algorithms for finding a minimum BDD size cover of an incompletely specified function, assuming the variable ordering is fixed.In some algorithms based on BDDs, incompletely specified functions arise for which any cover of the function will suffice.Choosing a cover that has a small BDD representation may yield significant performance gains.We present a systematic study of this problem, establishing a unified framework for heuristic algorithms, proving optimality in some cases,and presenting experimental results. Thomas R. Shiple, Ramin Hojati, Alberto L. Sangiovanni-Vincentelli, Robert K. Brayton |
DAC | 3 |
| 1994 | Equivalences for Fair Kripke Structures
Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICALP | 5 |
| 1994 | Iterative algorithms for formal verification of embedded real-time systems
Felice Balarin, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1994 | Time-domain non-Monte Carlo noise simulation for nonlinear dynamic circuits with arbitrary excitations
Alper Demir 0001, Edward W. Y. Liu, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1994 | Measurement and modeling of MOS transistor current mismatch in analog IC's
Eric Felt, Amit Narayan, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1994 | Testing of analog systems using behavioral models and optimal experimental design techniques
Eric Felt, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1994 | Techniques for crosstalk avoidance in the physical design of high-performance digital systems
Desmond Kirkpatrick, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1994 | A parallel iterative linear solver for solving irregular grid semiconductor device matricesabstractPresents the use of parallel processors for the solution of drift-diffusion semiconductor device equations using an irregular grid discretization. Preconditioning, partitioning and communication scheduling algorithms are developed to implement an efficient and robust iterative linear solver with preconditioning. The parallel program is executed on a 64-node CM-5 and is compared with PILS (a solver for ill-conditioned systems) running on a single processor. We observe an efficiency increase in obtaining parallel speed-ups as the problem size increases. We obtain 60% efficiency for CGS (a fast Lanczos-type solver for nonsymmetric linear systems) with no preconditioning for large problems. Using CGS with processor ILU preconditioning and magnitude threshold-fill-in preconditioning for the CM-5, and CGS with ILU for PILS, we attain 50% efficiency for the solution of large matrices.> Eric Tomacruz, Jagesh V. Sanghavi, Alberto L. Sangiovanni-Vincentelli |
SC | 3 |
| 1994 | Minimizing production test time to detect faults in analog circuitsabstractAnalog testing is a difficult task without a clearcut methodology. Analog circuits are tested for satisfying their specifications, not for faults. Given the high cost of testing analog specifications, it is proposed that tests for analog circuits should be designed to detect faults. Therefore analog fault modeling is discussed. Based on an analysis of the types of tests needed for different types of faults, algorithms for fault-driven test set selection are presented. A major reduction in testing time should come from reducing the number of specification tests that need to be performed. Hence algorithms are presented for minimizing specification testing time. After specification testing time is minimized, the resulting test sets are supplemented with some simple, possibly non-specification, tests to achieve 100% fault coverage. Examples indicate that fault-driven test set development can lead to drastic reductions in production testing time.> Linda S. Milor, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1994 | Circuit structure relations to redundancy and delayabstractThe existence of redundant stuck-faults in a logic circuit is potentially detrimental to high-speed operation, especially when there are false paths that are longer than the circuit delay. Keutzer, Malik, and Saldanha (KMS) in IEEE transactions of Computer Aided Design, vol. 10, no. 4, p. 427, April 1991 have proved that redundancy is not necessary to reduce delay by presenting an algorithm that derives an equivalent irredundant circuit from a given redundant circuit, with no increase in delay. The KMS algorithm consists of an iterative loop of timing analysis, gate duplications, and redundancy removal to successively eliminate long false paths. In this paper we resolve the main bottlenecks of the KMS algorithm by providing an efficient single-pass algorithm to simultaneously remove all long false paths from a given circuit. We achieve this by relating a circuit structure property based on path lengths to the testability (redundancy) and delay. The application of this algorithm to a variety of related logic synthesis problems is described.> Alexander Saldanha, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1994 | Satisfaction of input and output encoding constraintsabstractThree encoding problems relevant to the synthesis of digital circuits are input, output, and state encoding. Several encoding strategies have been proposed in the past that decompose the encoding problem into a two step process of constraint generation and constraint satisfaction. The latter requires the assignment of binary codes to symbols subject to the satisfaction of constraints on the codes. This paper focuses on the constraint satisfaction problem. We prove that constraint satisfaction is NP-complete. We develop a framework for the satisfaction of both input and output encoding constraints, and describe a polynomial time (in the number of symbols to be encoded) algorithm to check for the existence of a solution for a set of input and output constraints. An exact algorithm to determine the minimum number of encoding bits required to satisfy all the given constraints is provided, and a heuristic algorithm is also described. The application of this framework to a variety of encoding problems with different cost functions is illustrated. Experimental results on standard benchmarks are given for the exact and heuristic algorithms.> Alexander Saldanha, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1993 | An Iterative Approach to Language Containment
Felice Balarin, Alberto L. Sangiovanni-Vincentelli |
CAV | 2 |
| 1993 | A Verification Technique for Gated ClockabstractWe present a new model for circuits which have memory elements using conditional clocking, This is termed as the “gated” clock problem. Conventionally most of the recent efforts in timing analysis focus on memory elements controlled by clock signals only, We describe a simple restriction on the conditional signale which makes automatic verification easy. An algorithm to solve the timing verification problem for the case of restricted circuits based on previous approaches is given. Masamichi Kawarabayashi, Narendra V. Shenoy, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1993 | Circuit Delay Models and Their Exact Computation Using Timed Boolean FunctionsabstractIn this paper, we introduce a new circuit delay model, delay by sequences of vectors, which captures the essence of viability and floating delays. Then, we classify delays of circuits according to both the delay models of the gates making up the circuits and the family of inputs to the circuits. In this classification, we give sufficient conditions under which floating delay is the same as delay by sequences of vectors; these sufficient conditions are true for most practical circuits. This implies that the assumption of arbitrary node values used in the floating delay model is not too conservative. Thus, delay by sequences of vectors (hence, viability and floating delays), transition delay, and cycle time delay have coherent definitions under the same framework. Next, we study the problem of computing the exact circuit delays under both bounded and unbounded gate delay models, for some of which only upper bounds are known. By using a new formulation technique, called Timed Boolean Function, we formulate the problem of computing the exact delays as a mixed Boolean linear programming problem for which we give efficient algorithms to compute the exact delays of combinational circuit for transition delay and delay by sequences of vectors. The algorithms consider a subset of paths at one time and only the paths potentially responsible for the delay of a circuit are considered. Moreover, the core computation of the algorithms are composed of two computationally efficient algorithms: linear programming and BDD manipulations. We next compute floating (or viability) delays with the bounded gate delay model and show that delays by sequences of vectors and floating (or viability) delays are invariant under both bounded and unbounded gate delay models. Finally, we address the effect of gate delay lower bounds on delays of circuits. We demonstrate the effectiveness of the method by giving exact delay results for all ISCAS benchmark circuits (except C6188) William K. C. Lam, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1993 | Delay Fault Coverage and Performance TradeoffsabstractThe main disadvantage of the path delay fault model is that to achieve 100% testability every path must be tested.Since the number of paths is usually exponential in circuit size, atl known analysis and synthesis techniques for 100% path delay fault testability are infeasible on most circuits.In this paper, we show that 100'%odelay fault testability is not necessary to guarantee the speed of a combinational circuit.There exist path delay faults which can never impact the circuit delay (computed using arty correct timing analysis method) unless some other path delay faults also affect i~hence these delay faults need not be considered in delay fault testing.Next, assuming only the existence of robust delay fault tests for a very small set of paths, we show how the circuit speed can be selected such that 100% robust delay fault coverage is achieved. William K. C. Lam, Alexander Saldanha, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1993 | Analog System Verification in the Presence of Parasitics Using Behavioral SimulationabstractIn analog system design, final verification in the presence of parasitic loading effects is crucial to guarantee functionality of the entire circuit.In this paper, we present a methodology for analog system verification in the presence of parasitic using behavioral simulation.When applied to a synthesized 10 bit D/A, our approach is accurate to 0.005 LSB compared with SPICE, while being several orders of magnitude faster. Edward W. Y. Liu, Henry C. Chang, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1993 | Espresso-Signature: A New Exact Minimizer for Logic FunctionsabstractArticle Free Access Share on Espresso-signature: a new exact minimizer for logic functions Authors: Patrick McGeer View Profile , Jagesh Sanghavi View Profile , Robert Brayton View Profile , Alberto Sangiovanni Vincentelli View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 618–624https://doi.org/10.1145/157485.165069Online:01 July 1993Publication History 51citation464DownloadsMetricsTotal Citations51Total Downloads464Last 12 Months23Last 6 weeks5 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF Patrick C. McGeer, Jagesh V. Sanghavi, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1993 | Sequential Synthesis for Table Look Up Programmable Gate ArraysabstractArticle Sequential synthesis for table look up programmable gate arrays Share on Authors: Rajeev Murgai View Profile , Robert K. Brayton View Profile , Albert Sangiovanni-Vincentelli View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 224–229https://doi.org/10.1145/157485.164681Online:01 July 1993Publication History 13citation184DownloadsMetricsTotal Citations13Total Downloads184Last 12 Months1Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access Rajeev Murgai, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1993 | Resynthesis of Multi-Phase PipelinesabstractThis paper describes an algorithm for deriving necessa~andsufticient constraints for a multi-phase sequential pipeline to operate at a target clock cycle.Constraints on delays of the pipeline stages are used to drive a combinational logic delay optimizer to resynthesize the pipeline stagesfor improved performance.A main advantage of such an approach is that a global picture of the d~tribution of delays in the circuit is obtained.It also permits safe cycle stealing through level-sensitive latches acrosspipeline stages. Narendra V. Shenoy, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1993 | An algorithm for improving partitions of pin-limited multi-chip systemsabstractWe present a method for improving a topological partition of a logic circuit. Circuits are partitioned so that they may be implemented by a number of modules (for example, by a number of chips). By reducing the number of I/O pins necessary for communication between the modules we reduce the size of the chips needed to implement the modules, and thereby may also reduce the number of chips needed to implement the modules. Interpartition communication is organized into many unidirectional channels connecting the blocks. The number of lines necessary for implementing a communication channel is reduced by minimizing the amount of information that the channel must transmit, and by encoding the information that is transmitted. The reduction in the channel size usually is accompanied by an increase in the amount of logic in the partition modules. Thus this method is most effectively applied to design styles that are pin-limited; i.e. design styles that have a high ratio of logic area to number of input/output ports. We apply this method to a number of example communication channels and show large reductions in the size of the channels. We also show examples of designs that have fewer chips, or designs have smaller chips after application of these methods. Mark Beardslee, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1993 | Generalized constraint generation for analog circuit designabstractA general methodology is presented for the generation of a complete set of constraints on interconnect parasitics, parasitic mismatch and on the physical topology of analog circuits. The parasitic and matching constraints are derived from high-level performance specifications by means of sensitivity analysis in time and frequency domain using quadratic optimization. Topological constraints are obtained by using sensitivity and matching information on devices and interconnect as well as graph-based techniques to extract the necessary geometric information. Edoardo Charbon, Enrico Malavasi, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1993 | Nyquist data converter testing and yield analysis using behavioral simulationabstractThis paper presents a strategy for testing all DC performance of Nyquist data converters including offset error, full scale gain error, integral nonlinearity, and differential nonlinearity. In contrast to previous testing strategies based on linear models that require accurate measurements of circuit performance, our strategy uses a simpler measurement to verify that a circuit performance parameter falls within certain detection thresholds in the presence of measurement noise. Using the proposed strategy, we can evaluate tradeoffs between test set size, test coverage, detection thresholds, measurement noise, chip performance, and estimated yield. Our results support the obvious that smaller measurement noise, stricter detection thresholds, and lower chip performance would require smaller test set and reduce test time. Stricter detection thresholds, on the other hand, would decrease estimated yield. Edward W. Y. Liu, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1993 | Cube-packing and two-level minimizationabstractAlmost all mapping tools for programmable gate arrays (PGAs) start from a network optimized for the number of literals in the factored form. However, PGA architectures imposed different kinds of constraints on the synthesis process. For example, table look up (TLU) architectures restrict each function to at most m inputs (for a fixed m). This is unlike any type of constraint in PLA or standard-cell synthesis. Thus, standard cost functions like the number of cubes or factored form literals are not necessarily good complexity measures for TLU architectures. Decomposition and block count minimization are two steps in PGA mapping that are applied to an optimized design. In decomposition, a feasible representation of the network is obtained, which can be mapped directly onto the target architecture. Block count minimization then tries to maximally group the functions of the decomposed network into basic blocks such that the total number of blocks used are minimized. We address the problem of modeling the decompositon step, in optimization; in particular, we look at cube-packing, which has proved quite effective for the TLU architectures. We propose a technique for deriving a two-level representation of a logic function which yields better results after cube-packing. The technique rests on the idea of using the support of a set of primes as the basic object is two-level minimization, as opposed to a prime. Experiments indicate an average improvement of 12.5% over standard two-level methods. Rajeev Murgai, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1993 | Minimum padding to satisfy short path constraintsabstractCombinational circuits are often embedded in synchronous designs with memory elements at the input and output ports. A performance metric for a circuit is the cycle time of the clock signal. Correct circuit operation requires that all paths have a delay that lies between an upper bound and a lower bound. Traditional approaches in delay optimization for combinational circuits have dealt with methods to decrease the delay of the longest path. We address the issue of satisfying the lower bound constraints. Such a problem also arises in wave pipelining of circuits. We propose to handle short path constraints as a post processing step after traditional delay optimization techniques. There are two issues presented in this paper. We first discuss necessary and sufficient conditions for successful delay insertion without increasing delays of any long paths. In the second part, we present a naive approach to padding delays (greedy heuristic) and an algorithm based on linear programming. We describe an application of the theory to wave pipelining of circuits. Results are presented on a set of benchmark circuits, using two delay models. Narendra V. Shenoy, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1993 | Some Results on the Complexity of Boolean Functions for Table Look Up ArchitecturesabstractWe address the problem of determining the "complexity" of Boolean functions where complexity is measured as the minimum number of table look up blocks (TLUs) needed to implement a function. We present three new results. The first shows the exact value of the complexity of the class of (m+1)-input functions in terms of the TLUs with m inputs (m/spl ges/2). The next two derive upper bounds on the complexity, given some information about the representation of the function. One bound needs the number of literals and the number of cubes in a sum-of-products representation, and the other, the number of literals in a factored form. We compare these bounds with the results obtained by a TLU synthesis tool. On average, the factored form bounds are about 20% higher than the synthesized results, and hence are reasonable predictors of the number of TLUs needed. This prediction capability can be employed to quickly estimate, without performing any technology mapping, if a circuit can fit on one chip.> Rajeev Murgai, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCD | 3 |
| 1993 | Learning Complex Boolean Functions: Algorithms and Applications
Arlindo L. Oliveira, Alberto L. Sangiovanni-Vincentelli |
NIPS | 2 |
| 1993 | Architecture of field-programmable gate arraysabstractA survey of field-programmable gate array (FPGA) architectures and the programming technologies used to customize them is presented. Programming technologies are compared on the basis of their volatility, size parasitic capacitance, resistance, and process technology complexity. FPGA architectures are divided into two constituents: logic block architectures and routing architectures. A classification of logic blocks based on their granularity is proposed, and several logic blocks used in commercially available FPGAs are described. A brief review of recent results on the effect of logic block granularity on logic density and performance of an FPGA is then presented. Several commercial routing architectures are described in the context of a general routing architecture model. Finally, recent results on the tradeoff between the flexibility of an FPGA routing architecture, its routability, and its density are reviewed.> Jonathan Rose, Abbas El Gamal, Alberto L. Sangiovanni-Vincentelli |
Proc. IEEE | 3 |
| 1993 | Synthesis method for field programmable gate arraysabstractLogic synthesis algorithms and methods for field-programmable gate arrays (FPGAs) are reviewed. The three most popular types of FPGA architectures are considered, namely, those using logic blocks based on lookup-tables, multiplexers, and wide AND/OR arrays, respectively. The emphasis is on tools that attempt to minimize the area of the combinational logic part of a design, since little work has been done on optimizing performance or routability, or on synthesis of the sequential part of a design. The different tools surveyed are compared using a suite of benchmark designs.> Alberto L. Sangiovanni-Vincentelli, Abbas El Gamal, Jonathan Rose |
Proc. IEEE | 1 |
| 1993 | Two-Level Minimization of Multivalued Functions with Large OffsetsabstractExtends the theory of reduced offsets to logic functions with multivalued inputs. The authors show that the use of multivalued reduced offsets provides the same flexibility that is available with the use of the offset. Offset-based minimization of multivalued functions with large offsets often takes long computation time and requires very large memory and sometimes is not possible within reasonable time and memory. Such functions can be minimized effectively using reduced offsets.> Abdul A. Malik, Robert K. Brayton, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Computers | 4 |
| 1993 | Automated design management using tracesabstractAn automatic management system for CAD based on the idea that CAD tools can leave a trace of their execution is proposed. The trace, represented as a bipartite directed and acyclic graph in which the nodes represent either design data or tool invocations, is both a record of the design activity and a graph representing the dependencies among the design objects. The architecture of the proposed system is distributed. A server manages the trace, while a number of clients can concurrently interact with the trace through the server. The system is nonintrusive, because it does not affect the way designers interact with the tools. The design manager has been implemented in a system called VOV, which has been tested.> Andrea Casotto, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1993 | Automatic generation of parasitic constraints for performance-constrained physical design of analog circuitsabstractA design methodology for the physical design of analog circuits is proposed. The methodology is based on the automatic generation of constraints on parasitics introduced during the layout phase from constraints on the functional performance of the circuit. In this novel performance-constrained approach, the parasitic constraints drive the layout tools to reduce the need for further layout iterations. Parasitic constraint generation involves (1) generation of a set of bounding constraints on the critical parasitics of a circuit to provide maximum flexibility to the layout tools while meeting the performance constraints; and (2) deriving a set of matching constraints on the parasitics from matched-node-pair and matched-branch-pair information in differential circuits. The constraint generator PARCAR is described and results presented for test circuits.> Umakanta Choudhury, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1993 | Constraint-based channel routing for analog and mixed analog/digital circuitsabstractA well-defined methodology for mapping the constraints on a set of critical coupling capacitances into constraints in the vertical-constraint (VC) graph of a channel is presented. The approach involves directing undirected edges, adding directed edges, and increasing the weights of edges in the VC graph in order to meet crossover constraints between orthogonal segments and adjacency constraints between parallel segments while attempting to cause minimum increase in the channel height due to the constraints. Use is made of shield nets when necessary. A formal description of the conditions under which the crossover and the adjacency constraints are satisfied is provided and used to construct the appropriate mapping algorithms. The problem of imposing matching constraints on the routing parasitics in a channel with lateral symmetry is addressed. It is observed that perfect matching is not possible for a matched pair of nets with intersecting horizontal spans. A technique to achieve almost perfect mirror symmetry is presented for such pairs of nets.> Umakanta Choudhury, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1993 | Area routing for analog layoutabstractAn area router specifically tailored for the layout of analog circuits is presented. It is based on the A* algorithm, which combines the flexibility of maze routing with computational efficiency. Parasitics are controlled by means of a programmable cost function based on a set of user-defined weights. The weights can be automatically defined based on high-level electrical performance specifications and determine the net scheduling. An algorithm for symmetric routing preserves symmetries in differential architectures. Different current paths can be dealt with in each wire by means of a net partitioning procedure driven by information on the current driven by terminals. Shields can be built between critically coupled wires, in order to guarantee an effective limitation of cross-coupling. The weight-driven programmable cost function makes this router particularly suitable for a performance-driven approach to analog routing. Automatic weight definition also makes the use of the tool independent of the user's expertise. The implemented algorithms are described, and results proving the effectiveness of this approach are given.> Enrico Malavasi, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1993 | Performance optimization of pipelined logic circuits using peripheral retiming and resynthesisabstractThe problem of minimizing the cycle time of a given pipelined circuit is considered. The idea of simultaneous retiming and resynthesis is used to optimize a pipelined circuit to meet a given cycle time. An instance of the pipelined cycle optimization problem is specified by the circuit, a set of input arrival times relative to the clock, a set of required output times relative to the clock, and a given cycle time that it must meet. Given the instance of the pipelined performance optimization problem, the authors construct an instance of a combinational speedup problem. This is specified by a combinational logic circuit, a set of arrival times on the inputs, and a set of required times for the outputs which must be met. A constructive proof that the pipelined problem has a solution if and only if the combinational problem has a solution is given. This result shows that it is enough to consider only the combinational speedup problem, and all known techniques for that can be directly applied to generate a solution for the pipelined problem.> Sharad Malik, Kanwar Jit Singh, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1993 | ESPRESSO-SIGNATURE: a new exact minimizer for logic functionsabstractWe present a new algortthrn for exact two-ievei logzc opttmwatton which radtcally tmproves the Qutne -McCluskey (QM) procedure.The new aigorithm derzves the coverzng problem directly and amplicttly without generat~ng the set of all prtme zmplzcants.It then generates only those prime tmpltcants tnvolved in the covertng problem.We represent a set of primes by the Patrick C. McGeer, Jagesh V. Sanghavi, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Very Large Scale Integr. Syst. | 4 |
| 1992 | Solving the State Assignment Problem for Signal Transition Graphs
Luciano Lavagno, Cho W. Moon, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1992 | An Improved Synthesis Algorithm for Multiplexor-Based PGA's
Rajeev Murgai, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1992 | Equivalence of Robust Delay-Fault and Single Stuck-Fault Test Generation
Alexander Saldanha, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1992 | Circuit Structure Relations to Redundancy and Delay: The KMS Algorithm Revisited
Alexander Saldanha, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1992 | On the Temporal Equivalence of Sequential Circuits
Narendra V. Shenoy, Kanwar Jit Singh, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1992 | Automatic compositional minimization in CTL model checkingabstractA method for reducing the complexity of CTL model checking on a system of interacting finite state machines is described. The method consists essentially of reducing each component machine with respect to the property to be verified, and then verifying the property on the composition of the reduced components. The procedure is fully automatic and produces an exact result. The potential of the approach is assessed on real-world examples, and the method is demonstrated on a circuit.> Massimiliano Chiodo, Thomas R. Shiple, Alberto L. Sangiovanni-Vincentelli, Robert K. Brayton |
ICCAD | 3 |
| 1992 | Valid clocking in wavepipelined circuitsabstractAn analysis of valid clock rates in wavepipelined circuits using a technique called timed Boolean functions is presented. It is shown that the valid intervals for the clock period can be disconnected. Thus, it is insufficient to known only the minimum valid clock period in guaranteeing proper operation of pipelined circuits. Analytic expressions for the valid clock intervals in terms of both topological delay and two-vector longest and shortest delays are provided. Also uncertainties arising from manufacturing are taken into account. Some potential difficulties in computing the exact valid clock intervals are illustrated by demonstrating discontinuity and nonmonotonicity of the harmonic number H( tau ) (the number of valid simultaneous data waves allowed) as a function of the clock period tau .> William K. C. Lam, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1992 | Behavioral simulation for noise in mixed-mode sampled-data systemsabstractA direct noise analysis approach for mixed-mode systems is presented with experimental results compared with results from the traditional Monte Carlo approach. The direct approach computes noise effects by performing arithmetic on moments of distribution functions that characterize electronic noise. One key advantage of this approach is its ability to compute low error probabilities. From experimental results, it is shown that very low order moments, such as second order, are sufficient for a good estimate of noise effects.> Edward W. Y. Liu, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1992 | Graph algorithms for clock schedule optimizationabstractFor performance-driven synthesis of sequential circuits, the optimal clocking problem is considered, and it is shown that it is reducible to a parametric shortest path problem. Constraints are used that take into account both the short and long paths. The main contributions are efficient graph algorithms to solve the set of constraints necessary for correct clocking.> Narendra V. Shenoy, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1992 | A unified signal transition graph model for asynchronous control circuit synthesisabstractBoth low-level (analysis-oriented) and high-level (specification-oriented) models for asynchronous circuits and the environment where they operate, together with strong equivalence results between the properties at the low levels, are described. One interesting side result is the precise characterization of classical static and dynamic hazards in terms of the model. Consequently the designer can check the specification and directly decide if the behavior of any implementation will depend, e.g., on the delays of the signals described by such specification.> Alexandre Yakovlev, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1992 | Linear Programming for Optimum Hazard Elimination in Asynchronous CircuitsabstractIt is shown that hazards can be optimally eliminated from circuits synthesized starting with a signal transition graph (STG) specification. The proposed approach is based on a linear programming (or integer linear programming) formulation, and as such it can be solved efficiently and optimally for a variety of cost functions. Suggested cost functions optimize either the total padded delay, an estimate of the increase in area, or the maximum cycle time of the complete system. It is also shown that delay padding on all fanouts of STG signals is a necessary and sufficient condition for hazard elimination if the structure and delay of each combinational logic block cannot be changed. Experimental results indicate that the improvements obtained are well worth the added complexity of linear program solution.> Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
ICCD | 2 |
| 1992 | Sequential Circuit Design Using Synthesis and OptimizationabstractA description is given of SIS, an interactive tool for synthesis and optimization of sequential circuits. Given a state transition table or a logic-level description of a sequential circuit, SIS produces an optimized net-list in the target technology while preserving the sequential input-output behavior. Many different programs and algorithms have been integrated into SIS, allowing the user to choose among a variety of techniques at each stage of the process. It is built on top of MISII and includes all (combinational) optimization techniques therein as well as many enhancements. SIS serves as both a framework within which various algorithms can be tested and compared and as a tool for automatic synthesis and optimization of sequential circuits.> Ellen Sentovich, Kanwar Jit Singh, Cho W. Moon, Hamid Savoj, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCD | 6 |
| 1992 | Constructive Induction Using a Non-Greedy Strategy for Feature Selection
Arlindo L. Oliveira, Alberto L. Sangiovanni-Vincentelli |
ML | 2 |
| 1992 | Symbolic minimization of multilevel logic and the input encoding problemabstractTechniques for the optimization of multilevel logic with multiple-valued input variable is presented. The motivation for this is to tackle the input encoding problem in logic synthesis, where binary codes must be found for the different values that a symbolic input variable can take. It is shown how the other multilevel optimization techniques are easily extended with multiple-valued variables. These ideas have been implemented as algorithms in the program MIS-MV. The practical issues involved in the implementation of these ideas are discussed, and results of using MIS-MV for input encoding on benchmark examples presented.> Sharad Malik, Luciano Lavagno, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1991 | Algorithms for Synthesis of Hazard-Free Asynchronous CircuitsabstractA technique for the synthesis of asynchronous sequential circuits from a Signal Transition Graph (STG) specification is described. We give algorithms for synthesis and hazard removal, able to produce hazard-free circuits with the bounded wire-delay model, requiring the STG to be live, safe and to have the unique state coding property. A proof that, contrary to previous beliefs, STG persistency is not necessary for hazard-free implementation is given. 1 Introduction Asynchronous design is important in several applications of digital design. "Real world" interfaces and low power systems, where "lazy evaluation" style designs may extend the average life of a battery, are two examples. In addition, clock skew problems limit the performance and the flexibility of large scale synchronous systems. On the other hand asynchronous design is harder and more constrained than synchronous design, due to the hazard problem: asynchronous circuits are by definition sensitive to all signal changes, whe... Luciano Lavagno, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1991 | A Framework for Satisfying Input and Output Encoding ConstraintsabstractThree relevant encoding problems are input, output and state encoding.Several algorithms have been proposed for their solutions that decompose the problem into symbolic minimization (yielding a set of constraints) and constraint satisfaction.At least two exact formulations of the input encoding constraint satisfaction problem exist.However, a more important use of encoding is in state assignment of finite state machines where both input and output encoding constraints must be satisfied to obtain the most effective implementations.We develop a framework for the simultaneous satisfaction of input and output encoding constraints.We describe an algorithm, polynomial in the number of symbols to be encoded, to check for the existence of a solution for a set of input and output constraints.We provide an efficient atgorithm that determines the minimum number of encoding bits required to satisfy all the given constraints.We demonstrate how heuristic algorithms can be developed within the framework.Firtatly, we discuss the use of this framework in solving a variety of encoding problems with different cost functions.Some preliminary results on medium sized machines are given for both exact and heuristic algorithms. Alexander Saldanha, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
DAC | 4 |
| 1991 | Testability Solutions: Who Really Wants Them? (Panel Abstract)
Alberto L. Sangiovanni-Vincentelli |
DAC | 1 |
| 1991 | Synthesis for Testability Techniques for Asynchronous CircuitsabstractThe authors present techniques which guarantee both hazard-free operation and hazard-free robust path-delay-fault testability at the expense of possibly adding test inputs. They also give a set of heuristics which can improve hazard-free robust path-delay-fault testability without requiring such inputs. Finally, they demonstrate the effectiveness of these techniques on a set of asynchronous interface circuits gathered from industry and academia.> Kurt Keutzer, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1991 | A Behavioral Representation for Nyquist Rate A/D ConvertersabstractThe authors present a behavioral representation for the class of Nyquist rate A/D (analog-to-digital) converters. The representation captures the nominal A/D behavior as well as all the statistical variations. The variations are classified into noise and process variations according to how these nonidealities affect the A/D behavior. To describe noise effects a joint probability density function is used. To describe behavioral effects due to process variations, use is made of a variance-covariance matrix, Sigma /sub t/, which is a generalization of the integral nonlinearity vector. Sigma /sub t/'s rank characterizes the testability of an A/D; its decomposition yields efficient strategies for A/D testing. Finally, parameter extraction results obtained from prototypes are presented.> Edward W. Y. Liu, Alberto L. Sangiovanni-Vincentelli, Georges Gielen, Paul R. Gray |
ICCAD | 2 |
| 1991 | Performance Enhancement through the Generalized Bypass TransformabstractThe authors introduce a novel method for the acceleration of general logic circuits based on the assumption that the delay of a circuit is its longest sensitizable (non-false) path. Hence, circuits are accelerated not by reducing path length but by making paths false. The method is based on generalizing the transformation used to obtain the bypass adder to automatically, in an area efficient way, reduce the delay of any combinational logic circuit with paths of varying length. The authors prove that a circuit realizing any function can be accelerated in this manner, give a general algorithm, and prove bounds on the size of the gain expected.> Patrick C. McGeer, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli, Sartaj Sahni |
ICCAD | 3 |
| 1991 | Timing Analysis and Delay-Fault Test Generation using Path-Recursive FunctionsabstractThe authors introduce an efficient method for generating the functional forms of path analysis problems. They demonstrate that the resulting function is linear in the size of the circuit. The functions are then tested for satisfiability either using a Boolean network satisfiability algorithm suggested by T. Larrabee (1989) or through the construction of BDDs. The effectiveness of the proposed approach is shown for timing analysis and robust path delay-fault test generation. This method also holds promise for both static and dynamic hazard analysis, and for test generation using all other delay-fault models, tau -irredundant fault models, and stuck-open fault models.> Patrick C. McGeer, Alexander Saldanha, Paul R. Stephan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 5 |
| 1991 | On Clustering for Minimum Delay/AreaabstractThe authors address the problem of clustering a circuit for minimizing its delay, subject to capacity constraints on the clusters. They present an algorithm for combinational circuits and give sufficient conditions under which it is optimum. In addition, they address the problem of minimizing the number of clusters and nodes without increasing the maximum delay found by the algorithm. Finally, they extend the clustering algorithm to minimize the clock cycle of a sequential synchronous circuit.> Rajeev Murgai, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 3 |
| 1991 | Improved Logic Synthesis Algorithms for Table Look Up ArchitecturesabstractThe authors address the problem of synthesis for a popular class of programmable gate array architecture-the table look-up architectures. These use lookup table memories to implement logic functions. The authors present improved techniques for minimizing the number of table look up blocks used to implement a combinational circuit. On average, the results obtained on a set of benchmarks are 15-29% better than results obtained by previous approaches.> Rajeev Murgai, Narendra V. Shenoy, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1991 | Performance Directed Synthesis for Table Look Up Programmable Gate ArraysabstractThe authors address the problem of delay optimization for programmable gate arrays. The main considerations are the number of levels in the circuit and the wiring delay. The authors propose a two-phase approach: the first phase involves delay optimizations during logic synthesis before placement, while the second uses logic resynthesis in the case of a timing-driven placement technique. Results and comparisons on benchmarks are presented.> Rajeev Murgai, Narendra V. Shenoy, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 4 |
| 1991 | LSAT-An Algorithm for the Synthesis of Two Level Threshold Gate NetworksabstractThe authors present an algorithm for the synthesis of two-level threshold gate networks inspired by techniques used in classical two-level minimization of logic circuits. They specifically address a restricted version of the problem where the on and off set minterms are explicitly listed. Experimental results show that a simple branch and bound algorithm can be used to obtain solutions close to the absolute minimum in a set of standard problems, outperforming other minimizers even when restricted to using only classic logic gates as building blocks. The algorithm has a run time polynomial in the input size and its performance degrades slowly with the size of the problem.> Arlindo L. Oliveira, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 2 |
| 1991 | Retiming of Circuits with Single Phase Transparent LatchesabstractAn algorithm is developed for the retiming of single phase sequential circuits with level sensitive (transparent) latches. A set of constraints that permit retiming and optimal clock cycle computation are also developed. It is shown that a design with edge-triggered latches may be tested for speed-up using transparent latches.> Narendra V. Shenoy, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
ICCD | 3 |
| 1991 | Learning Concepts by Synthesizing Minimal Threshold Gate Networks
Arlindo L. Oliveira, Alberto L. Sangiovanni-Vincentelli |
ML | 2 |
| 1991 | A Theoretical Framework for Simulated Annealing
Fabio Romeo, Alberto L. Sangiovanni-Vincentelli |
Algorithmica | 2 |
| 1991 | Editor's Foreword
Alberto L. Sangiovanni-Vincentelli |
Algorithmica | 1 |
| 1991 | A macromodeling algorithm for analog circuitsabstractA macromodel is an electrical network containing fewer devices and/or fewer nodes than the circuit it represents. A general-purpose algorithm for the generation of macromodels suitable for circuit simulation is presented. The algorithm is based exclusively on a comparison of the input-output behavior of the macromodel with that to the circuit to be modeled. Because no reliance on any particular properties of the circuit is made, the algorithm can be used to model a very wide class of circuits. Three examples are presented to demonstrate the algorithm's performance, two of which were chosen specifically to test the algorithm's ability to approximate nonlinearities in the circuits to be modeled. In all cases, the accuracy of the macromodels was shown to improve substantially using reasonable amounts of CPU time.> Giorgio Casinovi, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1991 | Reduced offsets for minimization of binary-valued functionsabstractA modified approach to two-level logic minimization is described which obviates the need to compute the offset, yet provides the same global picture available with the offset. This approach is based on a new concept called the reduced offset. It is shown that reduced offsets can be computed without using the offset. This scheme has been implemented in ESPRESSO with an interface to the multilevel minimization environment MIS, where it is used to minimize individual nodes (representing two-level functions with single outputs) in multilevel networks. Such functions usually have very large offsets because of a large number of variables in their don't care sets. The modified approach is up to 8.5 times faster than ESPRESSO on a set of benchmark examples.> Abdul A. Malik, Robert K. Brayton, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |