System-on-chip security architecture is a critical, complex, and time-consuming activity, consuming months of effort. Furthermore, the architectural design can include subtle errors that compromise the security of the entire system. In this article, we develop a security engine infrastructure, SEnTry , for systematically creating security architectures for protecting SoC designs against a variety of security subversions. SEnTry provides a plug-and-play, configurable subsystem composed of custom IPs that can be integrated into the platform to derive different security primitives. We develop an instance of SEnTry for supply-chain attacks. We discuss the spectrum of challenges involved in developing a unified architecture for systematic protection against the variety of attacks involved and the SEnTry approach to addressing them. We provide several case studies to demonstrate SEnTry design and perform extensive experiments to evaluate its overhead on multiple ASIC technologies. Our experiments suggest that SEnTry incurs minimal overhead in area and power consumption.

Modern system-on-chip (SoC) designs are increasingly vulnerable to supply chain threats such as counterfeiting, overproduction, and reverse engineering, leading to financial losses, intellectual property (IP) theft, and compromised system integrity. Existing security engines, while effective in principle, typically rely on microcontroller-based architectures that incur significant area and power overhead, making them impractical for resource-constrained devices. In this article, we present a minimally configured security engine (MCSE), a lightweight, modular, configurable security engine designed to address the most critical supply-chain threats with minimal resource consumption. We introduce the notion ofminimum security, a baseline set of protection features necessary to secure SoCs under strict area and power constraints, and demonstrate how MCSE can be tailored to meet diverse system requirements. We validate our architecture through implementation on multiple ASIC technology nodes, showing favorable tradeoffs between security capability, area, and power. Our results establish MCSE as a compelling solution for integrating supply chain protection into low-power and area-sensitive SoC designs.

Steer-by-Wire (SbW) systems revolutionize automotive technology by eliminating the mechanical linkage between the steering wheel and tires, enhancing design flexibility and performance, especially in autonomous vehicles. However, this reliance on sensors and electronic data channels introduces critical security vulnerabilities. Exposed sensor locations in modern vehicles increase susceptibility to cyberattacks and physical interference, yet prior research has largely overlooked SbW-specific threats, particularly position encoders. This paper is the first to experimentally analyze SbW security vulnerabilities, presenting a novel attack methodology that disrupts SbW sensors. Our findings demonstrate how these vulnerabilities can compromise steering operations, posing severe risks to vehicle dynamics and occupant safety. As autonomous vehicles eliminate manual intervention, addressing these security risks becomes urgent. This study lays a foundation for developing more resilient SbW systems, ensuring safer and more secure automotive technologies.

5G communication technology has become a vital component in a wide range of applications due to its unique advantages such as high data rate and low latency. While much of the existing research has focused on optimizing its efficiency and performance, security considerations have not received comparable attention, potentially leaving critical vulnerabilities unexplored. In this work, we investigate the vulnerability of 5G systems to bit-flipping attacks, which is an integrity attack where an adversary intercepts 5G network traffic and modifies specific fields of an encrypted message without decryption, thus mutating the message while remaining valid to the receiver. Notably, these attacks do not require the attacker to know the plaintext, and only the semantic meaning or position of certain fields would be enough to effect targeted modifications. We conduct our analysis on OpenAirInterface (OAI), an open-source 5G platform that follows the 3GPP Technical Specifications, to rigorously test the real-world feasibility and impact of bit-flipping attacks under current 5G encryption mechanisms. Finally, we propose a keystream-based shuffling defense mechanism to mitigate the effect of such attacks by raising the difficulty of manipulating specific encrypted fields, while introducing no additional communication overhead compared to the NAS Integrity Algorithm (NIA) in 5G. Our findings reveal that enhancements to 5G security are needed to better protect against attacks that alter data during transmission at the network level.

Understanding automotive security becomes more significant as the probability of the average person interacting with an autonomous vehicle accelerates— Yet, only a small group of specialized experts understands the nuances of security in automotive systems. With this paper, we address this knowledge gap by developing an exploration platform that provides hands-on experience with wheel speed sensors (WSS) and their security weaknesses. Unlike previous research that based such exploration platforms solely on hardware or exclusively on virtual reality, this platform combines the two. Users, from students to industry professionals, may experience different wheel speed sensor attacks from the attacker and victim perspectives in a virtual environment built with Unity, a game development engine. The experience uses data from a wheel speed sensor model and a solenoid attacker module coded with Arduino. We describe the development process for this wheel speed sensor exploration platform and demonstrate how it might be used to understand different attack vectors, including a new spoofing attack developed with the platform that allows the attacker to accurately control the wheel speed with a PID controller and spoofed magnetic pulses. The platform serves as a medium for researchers to create and defend against new attacks and as an educational resource to expand knowledge in the automotive security field.

Logic Equivalence Checking (LEC) is a widely used formal verification method that ensures design accuracy by comparing implemented schematics with the respective Register Transfer Level (RTL) specifications to confirm functional equivalence. Traditional LEC approaches based on SAT-based verification often do not account for complexities introduced by resynthesis, technology transition, and port name changes, leading to verification failures or poor results. Additionally, IP protection techniques, including state space transformation and fine-grained redaction, further complicate traditional LEC analysis by altering the design and obscuring functional relationships, often leading to verification failures. This paper presents a novel framework, CLIP, Cut Point Matching-based Logic Equivalence Checking, that addresses these limitations of conventional LEC techniques and offers scalable and robust verification with higher accuracy and reliability leveraging on structural analysis. Experimental results show that CLIP can effectively handle both combinational and sequential designs, including support for transformed designs for which traditional LEC analysis fails, and significantly improves both verification efforts and accuracy for diverse open-source designs.

The rapid advancement of artificial intelligence (AI) has resulted in creation of a vast array of accelerator hardware, including GPUs, TPUs, and FPGAs, alongside the latest ASICs, to efficiently train and deploy AI models. However, AI accelerators are vulnerable to security threats that can compromise sensitive information, such as model architecture and jeopardize operational integrity, leading to unreliable applications. While significant efforts have been made for security verification of AI accelerators, existing techniques have inherent limitations and struggle to keep pace with evolving attack strategies. In this paper, we present a comprehensive analysis of the evolving field of security verification methodologies for AI accelerators, critically examining their effectiveness and identifying key limitations. Furthermore, we explore emerging trends in the field and outline potential research directions that could be pursued to enhance the security verification of AI accelerators.

Digital twin technology initially marked its presence in production and engineering, subsequently revolutionizing the healthcare sector with its groundbreaking applications. These include the creation of virtual replicas of patients and medical devices, enabling the formulation of personalized treatment plans. The rise of microcomputing, miniaturized hardware, and advanced machine-to-machine communications has laid the foundation for the Internet-of-Medical Things (IoMT), significantly transforming patient care through remote monitoring and timely diagnostics. Amid these technological strides, this paper offers a systematic review of digital twin technology’s integration within healthcare IoT, underlining its crucial role in promoting personalized medicine and tackling the pressing security challenges inherent in healthcare IoT systems. Focusing solely on the growing field of smart healthcare systems powered by IoT infrastructure, we explore the use of digital twins in digital patient modeling, the lifecycle of smart hospitals, surgical planning, medical devices, the pharmaceutical industry, and the IoMT cyber infrastructure, demonstrating their transformative potential in modern healthcare. Building on these findings, we outline key technical implications and emerging trends, highlight current challenges, and propose future research directions to advance healthcare IoT and its digital twin applications.

Network-on-Chip (NoC) fabrics are widely used in modern System-on-Chip designs to provide coordination among integrated hardware units. A significant category of security flaws entails a rogue foundry manipulating the routing logic and NoC topology through reverse engineering. In this study, we develop an architecture to defend NoC fabrics against these kinds of attacks, called OBNoCs [1] which replaces router connections in a reconfigurable manner with switches that may be configured to induce the desired topology after manufacturing. We achieve verifiable redaction of NoC functionality with our approach: switch configurations create several permissible topologies, but only one of them is the desired topology. We implement the OBNoCs technique on the Intel QuartusTM Platform, and experimental findings on practical SoC designs demonstrate that the architecture has low overhead related to power consumption and resource usage.

Consider a fleet of autonomous vehicles traversing an adversarial terrain that includes obstacles and mines. The goal of the fleet is to ensure that they can complete their mission safely (with minimal casualty) and efficiently (as quickly as possible). In Distributed Coordinated Fleet Management (DCFM), fleet members coordinate with one another while traversing the terrain, e.g., a vehicle encountering an obstacle at a location l can inform other agents so that they can recompute their route to avoid l. In this paper, we consider the problem of cyber-resilient DCFM, i.e., DCFM in an environment where the adversary can additionally tamper with the cyber-communication performed by the fleet members. Our framework, DRiFt, enables fleet members to coordinate in the presence of such adversaries. Our extensive evaluations demonstrate that DRiFt can achieve a high degree of safety and efficiency against a large spectrum of communication adversaries.

Deep learning systems are susceptible to evasion attacks, which represent a significant category of security vulnerabilities. These attacks entail the alteration of input data in such a way that the victim deep neural network (DNN) misclassifies it. Researchers have devised detection and defense methods to counter evasion attacks; however, these techniques impose a significant computational burden and are not suitable for real-time detection on devices with limited resources. This article presents an infrastructure,${\mathrm{G{\scriptstyle ERALT}}}$designed to improve the efficiency of evasion attack detection for real-time execution on edge devices. It involves a partition analysis that optimizes detection methods and allows for the use of a smaller detection network. Additionally, we propose a hardware architecture that accelerates internetwork inference using intermediate data reuse techniques and enables a different pattern of model updates between cloud servers and edge devices in real-world applications. Furthermore, it is also extended to a principle of internetwork accelerator design, which is evaluated at different PE ratios. Our evaluations demonstrate that${\mathrm{G{\scriptstyle ERALT}}}$achieves more than$3\times $improvement in performance compared to standard accelerators like Eyeriss, without affecting detection and classification accuracy. The boosted model update system avoids the bandwidth limit between edge devices and the cloud server, saving 14 h when updating the model for a new evasion attack.

Modern application-specific System-on-Chip designs include a variety of accelerator blocks that customize microcontrollers with domain-specific instruction sets and optimized microarchitectures. Unfortunately, accelerator implementations can be highly error-prone, undermining the reliability and security of the entire system. In spite of recent successes in formal methods, full verification of a complex accelerator microarchitecture is still beyond the scope of state-of-the-art formal technologies. In this paper, we address this problem through a novel methodology for incremental verification that can be tightly integrated with the design process. Our approach depends on a new foundation for microarchitecture correctness that enables viewing microarchitecture features as program transformations in a compiler design. The foundations enable designing microarchitecture features as incremental, semantics-preserving optimizations. We show how to use the foundations to develop correct-by-construction implementations of various advanced features of modern microprocessors. We demonstrate the viability of the foundations in designing correct-by-construction methodology for a superscalar microarchitectural implementation of the Versatile Tensor Accelerator.

Modern System-on-Chip functionalities include significant software interacting closely with low-level hardware to realize system functionalities. This software is developed concurrently with the hardware and must be validated before the hardware is fabricated. Current industrial practice depends on the creation of virtual prototyping environments to enable the validation of such software. However, creating such prototypes is complicated, manual, and error-prone. In this paper, we propose a novel infrastructure, for automatically generating virtual prototyping environments. includes an architecture and CAD flow to integrate different design blocks available in different abstraction levels to create a coherent, uniform view of SoC functionality suitable for early software validation. We show several case studies illustrating the applicability of .

Modern System-on-Chip (SoC) designs comprise hundreds of individual IP blocks, each with its custom implementation of reset signals in most cases. The asynchronous nature of these resets while crossing different reset domains makes the SoC prone to various vulnerabilities if not implemented and validated thoroughly. A key aspect in validating system functionality is to ensure the functionality under reset is verified. Traditional simulation-based validation techniques often become a bottleneck in complex SoC designs due to the large control path of these designs. We propose SoCCAR, a SoC validation framework that addresses this problem. SoCCAR leverages control flow graphs (CFG) of the design to extract the control flow associated with property violations caused by reset domain crossings due to asynchronous resets. SoCCAR efficiently tracks the chain of events leading to the payload without suffering from state space explosion, a common challenge in complex designs. We test the efficacy of SoCCAR in detecting such vulnerabilities by developing multiple SoC benchmarks, each embedded with custom vulnerability originating from reset implementations across different domains. These vulnerabilities reflect practical design complexity and correspond to security violations encountered in practice as a result of multiple asynchronous resets. SoCCAR successfully detected all violations with minimal computation overhead and runtime, making it a viable approach for detecting such violations in complex SoC designs.

Cooperative Adaptive Cruise Control (CACC) is a fundamental connected vehicle application. In CACC, a vehicle coordinates its longitudinal movements to safely and efficiently follow the vehicle in front. The follower vehicle relies on a combination of sensory and communication inputs to identify the position, velocity, and acceleration of the preceding vehicle. Malicious subversion of these inputs can cause catastrophic accidents, string instability, and disruption in the transportation infrastructure. In this paper, we develop a security system, ReCAP, to provide real-time resiliency in CACC against adversarial subversion of both sensory and communication inputs. ReCAP makes use of a combination of techniques based on kinematics and machine learning to detect anomalous inputs, narrow down the source of subversion, and perform mitigation. We provide extensive simulations to demonstrate the effectiveness of ReCAP against a diverse spectrum of attacks under complex, multi-channel adversaries.

We present an infrastructure for evaluating CNN models for vulnerability against a variety of integrity attacks. Our focus is on attacks that corrupt CNN computations with an impact on prediction/classification accuracy. The attack model encompasses a variety of mechanisms including injection of faults and glitches, integrity attacks on compute resources, etc. Our tool enables users to explore a variety of attack configurations, targets, and accuracy drops tolerated by the model. Experiments with our tool on publicly available CNN models show the vulnerability between layers is different, which can be exploited to protect important parts of the computation even when deployed on untrusted accelerators.

Evasion attacks constitute an important class of security vulnerabilities in deep learning systems. In this attack, the adversary can coerce the victim DNN into targeted misclassification with slightly modified input data. While detection and defense methods have been proposed for evasion attacks, they incur high overhead and cannot be employed for real time detection on resource-constrained devices. In this paper, we propose an infrastructure, Geralt, to optimize evasion attack detection for real-time execution. Geralt includes a software component to optimize detection methods enabling the use of a smaller detection network, and hardware architecture to accelerate inter-network inference with intermediate data reuse techniques. Our evaluation demonstrates that Geralt achieves more than 3x improvement in performance over standard accelerators like Eyeriss without affecting detection and classification accuracy.

Security is a critical challenge in emergent autonomous vehicles. However, the security challenges in automotive systems are not widely understood even in the cybersecurity community. To address this problem, we develop an adaptable exploration platform for automotive security. This platform enables users to gain hands-on experience and insights into security vulnerabilities. We discuss specific challenges and prerequisites involved in designing such an exploration tool. We demonstrate the platform's capabilities by exploring automotive ranging sensor attacks.

Modern autonomous vehicles are increasingly infused with sensors, electronics, and software software. One consequence is that they are getting increasingly susceptible to cyber-attacks. However, awareness of cybersecurity challenges for automotive systems remains low. In this paper, we consider the problem of developing a virtual reality (VR) infrastructure that can enable users who are not necessarily experts in automotive security to explore vulnerabilities arising from compromised ranging sensors. A key requirement for such platforms is to develop natural, intuitive scenarios that enable the user to experience security challenges and impact. We discuss the challenges in developing such scenarios, and develop a solution that enables exploration of jamming and spoofing attacks. Our solution is integrated into a VR platform for automotive security exploration called IVE (Immersive Virtual Environment). It combines realistic driving with a first-person view, user interaction, and sound effects to provide all the benefits of a real-life simulation without the consequences.

We consider the cybersecurity challenges arising from communications between autonomous vehicles and smart infrastructures. In particular, we consider coordination between vehicles and Reduced Speed Work Zones (RSWZ). Malicious or tampered communications between these entities can have catastrophic consequences. We discuss methods for the analysis of such attacks. In particular, we show how to generate configurable, effective vehicular trajectories for exploring such attacks and how to utilize such trajectories in identifying impactful attacks and evaluating defenses.

Vehicular communication systems and their applications have rapidly grown in recent years with the proliferation of cooperative applications. Unfortunately, vehicular network applications can be susceptible to cybersecurity attacks, disrupting the vehicular ecosystem or even causing fatal injuries. Unfortunately, platforms to enable realistic exploration of these vulnerabilities are limited. We address this critical need through the design of a new exploration platform, VeCAEP, to enable comprehension of communication attacks. VeCAEP permits the user to explore diverse communication attacks and comprehend interactions of different attack parameters and their impacts on the attack. We demonstrate VeCAEP with attacks on Cooperative Adaptive Cruise Control.

A critical requirement for robust, optimized, and secure design of vehicular systems is the ability to do system-level exploration, i.e., comprehend the interactions involved among electronic control units (ECUs), sensors, and communication interfaces in realizing system-level use cases and the impact of various design choices on these interactions. This must be done early in the system design to enable the designer to make optimal design choices without requiring a cost-prohibitive design overhaul. In this article, we develop a virtual prototyping environment for the modeling and simulation of vehicular systems. Our solution, ViVE, is modular and configurable, allowing the user to conveniently introduce new system-level use cases. Unlike other related simulation environments, our platform emphasizes coordination and communication among various vehicular components and just the abstraction of the necessary computation of each ECU. We discuss the ability of ViVE to explore the interactions between a number of realistic use cases in the automotive domain. We demonstrate the utility of the platform, in particular, to create real-time in-vehicle communication optimizers for various optimization targets. We also show how to use such a prototyping environment to explore vehicular security compromises. Furthermore, we showcase the experimental integration and validation of the platform with a hardware setup in a real-time scenario.

Multi-tenant applications have been proliferating in recent years, supported by the emergence of computing-as-service paradigms. Unfortunately, multi-tenancy induces new security vulnerabilities due to spatial or temporal co-location of applications with possibly malicious intent. In this article, we consider a special class of stealthy integrity attacks on multi-tenant deep learning accelerators. One interesting conclusion is that it is possible to perform targeted integrity attacks on kernel weights of deep learning systems such that it remains functional but mis-labels specific categories of input data through standard RowHammer attacks by only changing 0.0009% of the total weights. We develop an automated framework, AroMa , to evaluate the impact of multi-tenancy on security of deep learning accelerators against integrity attacks on memory systems. We present extensive evaluations on AroMa to demonstrate its effectiveness.

The push to meet growing user requirements and manufacturing challenges at lower technology nodes have motivated chip designers to adopt non-traditional design techniques. 2.5D/3DIC stacking has gained popularity in recent years since it enables chip manufacturers to integrate complex IPs to meet user demands without incurring design penalties. However, the non-traditional nature of the supply chain also means that additional challenges exist for verification and testing of the manufactured design, making the trust assurance of these designs an extremely challenging proposition. While there have been works focussing on securing 3DIC designs, very few address a completely untrusted supply chain. A robust security countermeasure must address the diverse trust requirements of the IPs in the design and the distributed supply chain requirements while ensuring that the functionality and performance overheads of the IC are not violated. We presentTREEHOUSE, a trust assurance solution to counter piracy, reverse-engineering, and counterfeiting attacks.TREEHOUSEuses scan authentication to detect piracy and counterfeiting, scan-and functional-locking to prevent reverse-engineering. We evaluate the efficiency of our proposed scheme on an example 3DIC design. We show thatTREEHOUSEincurs less than 1% area and power overheads while incurring less than 1% increase in overall gate count for each layer.

Driven by the rapid development of accelerators and diverse efficiency requirements of the naturally heterogeneous neural network computation, recent years have seen increased heterogeneity in neural network accelerator systems in terms of network structures, accelerator dataflows and implementations. However, existing research fails to schedule and map the heterogeneous neural networks on heterogeneous accelerators efficiently. They rely on clumpy exhaustive search or complicated ad hoc mapping approaches due to the semantic gap between the networks and accelerators. This paper proposes a systematic method to transform various accelerators into standard parameterized containers of the neural network loops, which builds a direct connection between the computation and the underlying hardware resources. This enables us to match the neural networks with accelerators based on their essential characteristics (e.g., reuse opportunities and bandwidth requirements) without diving into the detailed architectures. To this end, we propose AINNS, an all-inclusive neural network scheduler, that automatically schedules and maps the NN computation on heterogeneous accelerators with just one universal algorithm. Our experimental results show the proposed AINNS not only performs well in the traditional neural network acceleration but also improves the system throughput and energy efficiency by 1.8x and 1.7x respectively in the most challenging heterogeneous acceleration system.

Modern System-on-Chip (SoC) designs include a variety of Network-on-Chip (NoC) fabrics to implement coordination and communication of integrated hardware intellectual property (IP) blocks. An important class of security vulnerabilities involves a rogue hardware IP interfering with this communication to compromise the integrity of the system. Such interference includes message mutation, misdirection, delivery prevention, or IP masquerading, among others. In this article, we propose a scalable RTL-level SoC validation scheme, SeVNoC, for the systematic detection of security violations in inter-IP communications for SoC designs with NoC fabrics. Given a target security property to be validated, SeVNoC entails extraction of the control-flow graph of the relevant SoC, which is analyzed through a security property-based model comparison, without incurring state-space explosion. Our experiments on full-scale realistic SoC designs with multiple IPs and NoC architecture indicate that SeVNoC detects security violations in NoC communications with near-perfect accuracy, within only a few minutes.

Modern System-on-Chip designs typically use Network-on-Chip (NoC) fabrics to implement coordination among integrated hardware blocks. An important class of security vulnerabilities involves a rogue foundry reverse-engineering the NoC topology and routing logic. In this paper, we develop an infrastructure, ObNoCs , for protecting NoC fabrics against such attacks. ObNoCs systematically replaces router connections with switches that can be programmed after fabrication to induce the desired topology. Our approach provides provable redaction of NoC functionality: switch configurations induce a large number of legal topologies, only one of which corresponds to the intended topology. We implement the ObNoCs methodology on Intel Quartus™ Platform, and experimental results on realistic SoC designs show that the architecture incurs minimal overhead in power, resource utilization, and system latency.

We present an infrastructure, FirVer, for systematic validation of firmware binaries. FirVer makes unique use of virtual prototyping and unit testing interfaces for effective comprehension of hardware-firmware. We used FirVer on several library functions of TianoCore, a full-featured UEFI-compatible boot firmware developed by Intel Corporation. FirVer achieved more than 90% in line and function coverages, and between 60% and 80% branch coverage. FirVer also enabled exploration of corner cases that exposed segmentation faults in many constituent functions.

With the proliferation of connectivity and smart computing in vehicles, a new attack surface has emerged that targets subversion of vehicular applications by compromising sensors and communication. A unique feature of these attacks is that they no longer require intrusion into the hardware and software components of the victim vehicle; rather, it is possible to subvert the application by providing wrong or misleading information. We consider the problem of making vehicular systems resilient against these threats. A promising approach is to adapt resiliency solutions based on anomaly detection through Machine Learning. We discuss challenges in making such an approach viable. In particular, we consider the problem of validating such resiliency architectures, the factors that make the problem challenging, and our approaches to address the challenges.

Vehicles can utilize their sensors or receive messages from other vehicles to acquire information about the surrounding environments. However, the information may be inaccurate, faulty, or maliciously compromised due to sensor failures, communication faults, or security attacks. The goal of this work is to detect if a lane-changing decision and the sensed or received information are anomalous. We develop three anomaly detection approaches based on deep learning: a classifier approach, a predictor approach, and a hybrid approach combining the classifier and the predictor. All of them do not need anomalous data nor lateral features so that they can generally consider lane-changing decisions before the vehicles start moving along the lateral axis. They achieve at least 82% and up to 93% F1scores against anomaly on data from Simulation of Urban MObility (SUMO) [1] and HighD [2]. We also examine system properties and verify that the detected anomaly includes more dangerous scenarios.

The development of deep neural network (DNN) has provided transformative impacts on many fields, including computer vision and video recognition. However, the impact is limited by the need for large, labeled datasets to enable effective training. To address this fundamental problem, we propose a novel inter-network system (Dandelion), providing architecture support (Dandelion-architecture) for data augmentation that trains DNNs with rare images generated by the generative adversarial network (GAN) with orthogonal attributes modified (Dandelion-function. The approach can account for the latency requirement and resource limitation of target applications by exploiting data and computation reuses between the two networks; this amortizes the impact of bottleneck brought by GAN and facilitates design of inter-network accelerator. Moreover, we show how to implement two-network design on 3D architecture to further enhance the accelerator. Our results show that with the generated images, DNN yields 13.6% - 37.5% improvement on accuracy, depending on the data scarcity level. Our architecture achieves at least 30% speedup compared with the baseline while 40% of the overhead brought by the incorporation of GAN is reduced in our design compared with ScaleDeep, and 26.3% of performance improvement over TETRIS.

The acceleration of CNNs has gained increasing attention since their success in computer vision. Since the heterogeneous layers cannot be processed by accelerators proposed for convolution layers only, modern end-to-end CNN acceleration solutions either transform diverse computation into matrix/vector arithmetic, which loses data reuse opportunities in convolution, or introduce dedicated functional unit to each kind of layer, which results in underutilization and high update expenses. To enhance the whole-life cost efficiency, we need a solution that is efficient in processing CNN layers and has the generality to apply to all kinds of existing and emerging layers. To this end, we propose GCONV Chain, a method to convert the entire CNN computation into a chain of standard general convolutions (GCONV) that can be efficiently processed by existing CNN accelerators with low-overhead hardware support. This paper comprehensively analyzes the GCONV Chain model and proposes a full-stack implementation to support GCONV Chain. Our results on various CNNs demonstrate that GCONV Chain improves the performance and energy efficiency of existing CNN accelerators by an average of 3.4x and 3.2x respectively. Furthermore, we show that GCONV Chain provides low whole-life costs for CNN acceleration, including both developer efforts and total cost of ownership.

Cooperative Adaptive Cruise Control (CACC) is a fundamental connected vehicle application that extends Adaptive Cruise Control by exploiting vehicle-to-vehicle (V2V) communication. CACC is a crucial ingredient for numerous autonomous vehicle functionalities including platooning, distributed route management, etc. Unfortunately, malicious V2V communications can subvert CACC, leading to string instability and road accidents. In this paper, we develop a novel resiliency infrastructure, RACCON, for detecting and mitigating V2V attacks on CACC. RACCON uses machine learning to develop an on-board prediction model that captures anomalous vehicular responses and performs mitigation in real time. RACCON-enabled vehicles can exploit the high efficiency of CACC without compromising safety, even under potentially adversarial scenarios. We present extensive experimental evaluation to demonstrate the efficacy of RACCON.

We present CAD framework and EDA tool,$\mathrm{S{\scriptstyle O}CC{\scriptstyle OM}}$, for automated synthesis of optimized SoC architectures. We delineate a disciplined and streamlined methodology to enable automated IP integration and design optimization.$\mathrm{S{\scriptstyle O}CC{\scriptstyle OM}}$supports generation of a wide variety of optimized SoCs by: 1) automating the entire process of intellectual property (IP) standardization and integration; 2) allowing configurable assembly of complex, scalable systems with application-specific subsystems; and 3) enabling optimization and evaluation of generated designs based on area and power constraints. Applications of$\mathrm{S{\scriptstyle O}CC{\scriptstyle OM}}$include development of heterogeneous, domain-specific SoCs, rapid register-transfer level (RTL) prototyping of wide-varieties of SoC benchmarks, and many others.

Modern SoC designs include several reset domains that enable asynchronous partial resets while obviating complete system boot. Unfortunately, asynchronous resets can introduce security vulnerabilities that are difficult to detect through traditional validation. In this paper, we address this problem through a new security validation framework, SoCCCAR, that accounts for asynchronous resets. The framework involves (1) efficient extraction of reset-controlled events while avoiding combinatorial explosion, and (2) concolic testing for systematic exploration of the extracted design space. Our experiments demonstrate that SoCCAR can achieve almost perfect detection accuracy and verification time of a few seconds on realistic SoC designs.

Modern System-on-Chip (SoC) designs include a large number of embedded microcontrollers that execute custom firmware. Firmware provides the flexibility of updating security features, i.e., it enables patching or in-field update, in response to an emerging security threat, bug, or changing requirements. Unfortunately, current firmware update mechanisms are complex, manual, and error-prone. In this paper we present CASTLE, an architectural framework to enable systematic and assured updates to SoC firmware. The main workhorse of CASTLE is a centralized, dedicated IP in the SoC that is responsible for receiving, authenticating, and installing a patch. The architecture works with off-chip firmware validation flows, e.g., cloud-based service for validating a proposed patch, and identifying compatibility constraints on other resident firmware in the SoC. The result is a comprehensive infrastructure that works seamlessly across architectures, vendors, and service providers, while meeting deployment and usability requirements. We demonstrate the application of proposed framework in addressing functional and security flaws of existing firmware patching mechanisms including firmware incompatibility, inadequate authentication, and time-of-check vs. time-of-use (TOCTOU) constraints.

The goal of speed path validation is to identify frequency limiting paths in a fabricated IC. It is a complex and expensive activity, requiring significant manual expertise. This paper provides a tutorial overview of speed path validation, focusing primarily on the state of the practice and its limitations. This paper also discusses delay test and discusses synergies between the two disciplines.

Asset provisioning is a crucial step in present-day IC manufacturing process. The nature of on-chip assets can range from crypto keys, IC configurations, and manufacturer firmware to target specific security specifications, policies, and chip debugging information. Given the criticality of the assets, a major part of IC security research is targeted towards the development of their protection mechanisms, especially in post-fabrication deployment phase. However, in this work our curious observation is that a series of novel attack surfaces can stem from asset provisioning at untrusted testing sites and colluding foundries which are not covered by existing threat models and defense schemes. To that end, we study the state-of-the-art protection mechanisms adopted for secure IC provisioning at untrusted testing facilities and highlight their security vulnerabilities. In particular, we show the inadequacy of existing authentication and design obfuscation-based defense mechanisms during asset provisioning through a secure root of trust.

There is a recent trend that the DNN workloads and accelerators are increasingly heterogeneous and dynamic. Existing DNN acceleration solutions fail to address these challenges because they either rely on complicated ad hoc mapping or clumpy exhaustive search. To this end, this paper first proposes a formalization model that can comprehensively describe the accelerator design space. Instead of enforcing certain customized dataflows, the proposed model explicitly captures the intrinsic hardware functions of a given accelerator. We connect these functions with the data reuse opportunities of the DNN computation and build a correspondence between DNN loop blocking and accelerator constraints. Based on this, we implement an algorithm that efficiently and effectively performs universal loop blocking for various DNNs and accelerators without manual specifications. The evaluation shows that our results manifest 2.1x and 1.5x speedup and energy efficiency over dataflow-defined algorithm as well as significant improvement in blocking latency compared with search-based methods.

Modern System-on-Chip (SoC) designs integrate a number of third party IPs (3PIPs) that coordinate and communicate through a Network-on-Chip (NoC) fabric to realize system functionality. An important class of SoC security attack involves a rogue IP tampering with the inter-IP communication. These attacks include message snoop, message mutation, message misdirection, IP masquerade, and message flooding. Static IP-level trust verification cannot protect against these SoC-level attacks. In this paper, we analyze the vulnerabilities of system level communication among IPs and develop a novel SoC security architecture that provides system resilience against exploitation by untrusted 3PIPs integrated over an NoC fabric. We show how to address the problem through a collection of fine-grained SoC security policies that enable on-the-fly monitoring and control of appropriate security-relevant events. Our approach, for the first time to our knowledge, provides an architecture-level solution for trusted SoC communication through run-time resilience in the presence of untrusted IPs. We demonstrate viability of our approach on a realistic SoC design through a series of attack models and show that our architecture incurs minimal to modest overhead in area, power, and system latency.

System-on-Chip (SoC) security architectures targeted towards diverse applications including Internet of Things (IoT) and automotive systems enforce two critical design requirements: in-field configurability and low overhead. To simultaneously address these constraints, in this paper, we present a novel, flexible, and adaptable SoC security architecture that efficiently implements diverse security policies. The architecture and associated CAD flow enable “hardware patching” i.e. hardware security policy engine that can be seamlessly and securely upgraded in field to address unanticipated attacks or new security requirements. We implement (1) a centralized Reconfigurable Security Policy Engine (RSPE), (2) smart security wrappers, and (3) Design-for-Debug (DfD) infrastructure interface as the building blocks of the architecture. The proposed framework provides a systematic approach to represent and synthesize diverse security policies. Through extensive analysis using representative SoC models, we show, for the first time to our knowledge, that the proposed framework provides high level of patchability with minimal energy and performance overhead.

We present a method for selecting trace messages for post-silicon validation of Systems-on-a-Chips (SoCs) with diverse usage scenarios. We model specifications of interacting flows in typical applications. Our method optimizes trace buffer utilization and flow specification coverage. We present debugging and root cause analysis of subtle bugs in the industry scale OpenSPARC T2 processor. We demonstrate that this scale is beyond the capacity of current tracing approaches. We achieve trace buffer utilization of 98.96% with a flow specification coverage of 94.3% (average). We localize bugs to 21.11% (average) of the potential root causes in our large-scale debugging effort.

Modern automotive systems and IoT devices are designed through a highly complex, globalized, and potentially untrustworthy supply chain. Each player in this supply chain may (1) introduce sensitive information and data (collectively termed "assets") that must be protected from other players in the supply chain, and (2) have controlled access to assets introduced by other players. Furthermore, some players in the supply chain may be malicious. It is imperative to protect the device and any sensitive assets in it from being compromised or unknowingly disclosed by such entities. A key --- and sometimes overlooked --- component of security architecture of modern electronic systems entails managing security in the face of supply chain challenges. In this paper we discuss some security challenges in automotive and IoT systems arising from supply chain complexity, and the state of the practice in this area.

Modern system-on-chip (SoC) designs include a wide variety of highly sensitive assets which must be protected from unauthorized access. A significant aspect of SoC design involves exploration, analysis, and evaluation of resiliency mechanisms against attacks to such assets. These attacks may arise from a number of sources, including malicious intellectualproperty blocks (IPs) in the hardware, malicious or vulnerable firmware and software, insecure communication of the system with other devices, and side-channel vulnerabilities through power and performance profiles. Countermeasures for these attacks are equally diverse, which include architecture, design, implementation, and validation-based protection. In this paper, we provide a comprehensive overview of the security infrastructure in modern SoC designs, including both resiliency techniques and their validation paradigms at presilicon and postsilicon stages. We identify gaps in current resiliency and analysis architectures and propose design and validation solutions to address them. Finally, we provide industry perspectives on the role and impact of current practices on SoC security, and discuss some emerging trends in this important area.

Field Programmable Gate Arrays (FPGAs) are being increasingly deployed in diverse applications including the emerging Internet of Things (IoT), biomedical, and automotive systems. However, security of the FPGA configuration file (i.e. bitstream), especially during in-field reconfiguration, as well as effective safeguards against unauthorized tampering and piracy during operation, are notably lacking. The current practice of bitstreram encryption is only available in high-end FPGAs, incurs unacceptably high overhead for area/energy-constrained devices, and is susceptible to side channel attacks. In this paper, we present a fundamentally different and novel approach to FPGA security that can protect against all major attacks on FPGA, namely, unauthorized in-field reprogramming, piracy of FPGA intellectual property (IP) blocks, and targeted malicious modification of the bitstream. Our approach employs the security through diversity principle to FPGA, which is often used in the software domain. We make each device architecturally different from the others using both physical (static) and logical (time-varying) configuration keys, ensuring that attackers cannot use a priori knowledge about one device to mount an attack on another. It therefore mitigates the economic motivation for attackers to reverse engineering the bitstream and IP. The approach is compatible with modern remote upgrade techniques, and requires only small modifications to existing FPGA tool flows, making it an attractive addition to the FPGA security suite. Our experimental results show that the proposed approach achieves provably high security against tampering and piracy with worst-case 14% latency overhead and 13% area overhead.

A modern automotive design contains over a hundred microprocessors, several cyber-physical modules, connectivity to a variety of networks, and several hundred megabytes of software. The future is anticipated to see an even sharper rise in complexity of this electronics, with the imminence of driverless vehicles, the potential of connected automobiles within a few years, and work towards seamless integration of automobiles with smart cities and infrastructure systems. Security is a fundamental challenge in the design of automotive systems. Unfortunately, security considerations in automotive systems are complicated by two factors: (1) need for real-time mitigation against in-field threats; and (2) in-field configurability and extensibility of security features. This paper examines the trade-offs between security countermeasures, real-time requirements, and in-field configurability needs for modern automotive systems. We discuss the current state of the practice in automotive security architecture, as well as gaps and challenges that need to be addressed for a viable security solution in future.

The Transportation Sector is one of the Critical Infrastructure Sectors identified by the United States Department of Homeland Security. Developing robust, secure, and resilient designs for Transportation Sector components is particularly challenging since it requires significant, real-time coordination with automotive, marine, and aviation systems that are themselves undergoing transformative changes in electronic complexity. In this paper we provide a general overview of security challenges in the Transportation Sector, focusing in particular the Highways and Roadways sub-sector. We discuss current and emergent challenges in this area arising as a result of increased autonomy (and hence complexity) of automotive systems, and point out key research needs.

Reconstructing system-level behavior from silicon traces is a critical problem in post-silicon validation of System-on-Chip designs. Current industrial practice in this area is primarily manual, depending on collaborative insights of the architects, designers, and validators. This paper presents a trace analysis approach that exploits architectural models of system-level protocols to reconstruct design behavior from partially observed silicon traces in the presence of ambiguous and noisy data. The output of the approach is a set of all potential interpretations of a system's internal execution abstracted to system-level protocols. To support the trace analysis approach, a companion trace signal selection framework guided by system-level protocols is also presented, and its impacts on the complexity and accuracy of the analysis approach are discussed. That approach and the framework have been evaluated on a multi-core System-on-Chip prototype that implements a set of common industrial system-level protocols.

Modern system-on-chip (SoC) designs involve integration of a large number of intellectual property (IP) blocks, many of which are acquired from untrusted third-party vendors. An IP containing a security vulnerability-whether inadvertent or malicious-may compromise the trustworthiness of the entire SoC, e.g., by leaking sensitive information or causing execution failures at key points. Existing functional validation approaches, post-manufacturing tests, and IP trust verification techniques are inadequate to accomplish comprehensive system-level security assurance in the presence of untrusted IPs. In this paper, we analyze security issues at the SoC level caused by untrusted IPs. We also propose a novel, resilient SoC security architecture to ensure trusted SoC operation with untrusted IPs. Our architecture realizes fine-grained IP-trust aware security policies in an efficient security policy checker that enables run-time monitoring of security issues arising from untrusted IPs. It also exploits on-chip design-for-debug architecture to ensure trusted information flow from IP blocks to the security policy checker. Unlike existing solutions to the untrusted IP problem, which rely on verification of IP trust before they are integrated into an SoC, the proposed approach follows a fundamentally different architecture-level solution based on run-time resilience. We demonstrate the effectiveness of this framework for system protection using several illustrative practical use cases. We also provide experimental results to show that the overhead of the proposed architecture is modest on representative SoC designs.

A key problem in postsilicon validation is to identify a small set of traceable signals that are effective for debug during silicon execution. Structural analysis used by traditional signal selection techniques leads to a poor restoration quality. In contrast, simulation-based selection techniques provide superior restorability but incur significant computation overhead. In this paper, we propose an efficient signal selection technique using machine learning to take advantage of simulation-based signal selection while significantly reducing the simulation overhead. The basic idea is to train a machine learning framework with a few simulation runs and utilize its effective prediction capability (instead of expensive simulation) to identify beneficial trace signals. Specifically, our approach uses: (1) bounded mock simulations to generate training vectors for the machine learning technique and (2) a compound search-space exploration approach to identify the most profitable signals. Experimental results indicate that our approach can improve restorability by up to 143.1% (29.2% on average) while maintaining or improving runtime compared with the state-of-the-art signal selection techniques.

Systematic implementation of System-on-Chip (SoC) security policies typically involves smart wrappers extracting local security critical events of interest from Intellectual Property (IP) blocks, together with a control engine that communicates with the wrappers to analyze the events for policy adherence. However, developing customized wrappers at each IP for security requirements may incur significant overhead in area and hardware resources. In this paper, we address this problem by exploiting the extensive design-for-debug (DfD) instrumentation already available on-chip. In addition to reduction in the overall hardware overhead, the approach also adds flexibility to the security architecture itself, e.g., permitting use of on-field DfD instrumentation, survivability and control hooks to patch security policy implementation in response to bugs and attacks found at post-silicon or changing security requirements on-field. We show how to design scalable interface between security and debug architectures that provides the benefits of flexibility to security policy implementation without interfering with existing debug and survivability use cases and at minimal additional cost in energy and design complexity.

We present an outline of the field of Multilevel Design Understanding by first defining and motivating the related problems, and then describing the key issues which must be addressed in future research.

We are in the regime of Internet-of-Things (IoT), - a regime characterized by billions of smart, connected computing devices coordinating to provide large-scale, highly personalized applications. Two overriding themes in this regime are energy consumption and security enforcement, which are both critical to the sustainability and proliferation of the IoT ecosystem. However, energy and security requirements are often at odds. This paper discusses several challenges in developing trustworthy IoT devices that comprehend the energy-security trade-offs. We also outline some emergent approaches to address this conflict.

Internet of Things (IoT) is becoming prevalent in almost all aspects of our daily lives as well as in critical, infrastructures. The widely usage of IoT also breeds security and privacy concerns. In this session, we will discuss IoT security challenges related to unique validation challenges, low-cost IoT authentication solutions, and design for security in IoT space.

We consider the conflicts between requirements from security and post-silicon validation in SoC designs. Post-silicon validation requires hardware instrumentations to provide observability and controllability during on-field execution; this in turn makes the system prone to security vulnerabilities, resulting in potentially subtle security exploits. Mitigating such threats while ensuring that the system is amenable to post-silicon validation is challenging, involving close collaboration among security, validation, testing, and computer architecture teams. We examine the state of the practice in this area, the trade-offs and compromises made, and their limitations. We also discuss an emerging approach that we are contemplating to address this problem.

The lack of appropriate models is often the biggest hurdle in applying formal methods in the industry. Creating executable models of industrial designs is a challenging task, one that we believe has not been sufficiently addressed by existing research. We address this problem for distributed message passing protocols by showing how to synthesize executable models of such protocols from transaction message flows, which are readily available in architecture descriptions. We present industrial case studies showing that this approach to creating formal models is effective in practice. We also show that going the other way, i.e., extracting flows from executable models, is at least as hard as the model-checking problem. These results indicate that transaction flows may provide a superior approach to capture design intent than executable models.

Modern SoC designs incorporate several security policies to protect sensitive assets from unauthorized access. The policies affect multiple design blocks, and may involve subtle interactions between hardware, firmware, and software. This makes it difficult for SoC designers to implement these policies, and system validators to ensure adherence. Associated problems include complexity in upgrading these policies, IP reuse for systems targeted for markets with differing security requirement, and consequent increase in design time and time-to-market. In this paper, we address this important problem by developing a generic, flexible architectural framework for implementing arbitrary security policies in SoC designs. Our architecture has several distinctive features: (1) it relies on a dedicated, centralized, firmware-upgradable plug-and-play IP block that can implement diverse security policies; (2) it interfaces with individual IP blocks through their “security wrapper”, which exploits and extends test/debug wrappers; (3) it implements a security policy as firmware code following existing security policy languages; (4) it can implement any security policy as long as relevant observable and controllable signals from the constituent IPs are accessible through the security wrappers; and (5) it realizes a low-overhead communication link between security wrappers of IP blocks and the centralized, dedicated controller. The approach builds on and extends the recent work on developing a centralized infrastructure IP for SoC security, referred to as IIPS, that interface with IP blocks using their boundary scan based wrappers. While this architecture is generic and independent of security policy types, we provide case studies with several common policies to show the flexibility and extendibility of the architecture. We also evaluate its viability in terms of overhead in area and power.

State Restoration Ratio (SRR) has been the de facto standard for evaluating quality of signals selected for post-silicon tracing and debug. Given a set S of selected signals, SRR measures the fraction of (gate-level) design states that can be inferred from observing signals in S at each cycle. Unfortunately, in spite of its widespread use, we found that SRR is intrinsically unsuitable as a metric for evaluating trace signal quality, as it captures neither the higher-level functionality of the design nor the constraints and requirements on trace signals imposed by architectural, physical, or security requirements. In this paper, we argue with strong empirical evidence that SRR must be replaced by a metric that closely models high-level behavioral coverage. We propose assertion coverage as a first step in this direction. We also present a new algorithm, based on Pagerank, for post-silicon trace selection. Pagerank is not designed to maximize SRR. We found that Pagerank has upto 70% higher behavioral coverage than SRR optimizing methods, and the RTL PageRank has upto 30% higher behavioral coverage than the netlist PageRank algorithm. Assertion coverage of PageRank RTL is upto 50% while SRR based methods have less than 5% assertion coverage.

Modern SoC designs contain a large number of sensitive assets that must be protected from unauthorized access. Authentication mechanisms which control the access to such assets are governed by complex security policies. The security policies affect multiple design blocks and may involve subtle interactions among hardware, firmware, OS kernel, and applications. The implementation of security policies in an SoC design, often referred to as its security architecture, is a subtle composition of coordinating design modules distributed across the different IPs. Toward this direction, this paper gives an overview of SoC security architectures in modern SoC designs and provides a glimpse of their implementation, as well as their design complexities and functional shortcomings. Design of security architectures involves a complex interplay of requirements from functionality, power, security, and validation. We also outline some of the research needs in the area for developing robust, trustworthy SoC designs.

Behavioral synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a register-transfer level (RTL) implementation. In this paper, we present a scalable equivalence checking framework to validate the correctness of compiler transformations employed by behavioral synthesis front-end. Our approach makes use of dual-rail symbolic simulation of the input and output of a transformation, together with identification and inductive verification of their loop structures. We have evaluated our framework on transformations applied by an open source behavioral synthesis tool to designs from the CHStone benchmark. Our tool can automatically validate more than 75 percent of the total of 1008 compiler transformations applied, taking an average time of 1.5 seconds per transformation.

Function pipelining is a key transformation in behavioral synthesis. However, synthesizing the complex pipeline logic is an error-prone process. Sequential equivalence checking (SEC) support is highly desired to provide confidence in the correctness of synthesized pipelines. However, SEC for function pipelining is challenging due to the significant difference between the behavioral specification and synthesized RTL. Furthermore, function pipelines include hardware logic for dynamically inserting “bubbles” (pipeline stalls), which bring additional difficulties in equivalence checking. We develop an SEC framework for behaviorally synthesized function pipelines by (1) building a reference pipeline model with a certified function pipelining transformation, which faithfully captures bubble insertion; and (2) checking the equivalence between the reference model and synthesized RTL. We demonstrate the scalability of our approach on industry-strength designs synthesized by a commercial tool.

Behavioral synthesis involves generating hardware design via compilation of its Electronic System Level (ESL) description to an RTL implementation. Equivalence checking is critical to ensure that the synthesized RTL conforms to its ESL specification. Such equivalence checking must effectively handle design and implementation optimizations. We identify two key optimizations that complicate equivalence checking for behavioral synthesis: (1) operation gating, and (2) global variables. We develop a sequential equivalence checking (SEC) framework to compare ESL designs with RTL in the presence of these optimizations. Our approach can handle designs with more than 32K LoC RTL synthesized from practical ESL designs. Furthermore, our evaluation found a bug in a commercial tool, underlining both the importance of SEC and the effectiveness of our approach.

A key problem in post-silicon validation is to identify a small set of traceable signals that are effective for debug during silicon execution. Structural analysis used by traditional signal selection techniques leads to poor restoration quality. In contrast, simulation-based selection techniques provide superior restorability but incur significant computation overhead. In this paper, we propose an efficient signal selection technique using machine learning to take advantage of simulation-based signal selection while significantly reducing the simulation overhead. Our approach uses (1) bounded mock simulations to generate training vectors set for the machine learning technique, and (2) an elimination approach to identify the most profitable signals set. Experimental results indicate that our approach can improve restorability by up to 63.3% (17.2% on average) with a faster or comparable runtime.

Behavioral synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a Register-Transfer Level (RTL) implementation. We present a scalable equivalence checking framework to validate the correctness of compiler transformations employed by behavioral synthesis. Our approach is based on dual-rail symbolic simulation of the input and output design representations of a transformation. We have evaluated our framework on transformations applied to several designs by an open source behavioral synthesis tool, and we present initial results demonstrating the approach.

Loop pipelining is a critical transformation in behavioral synthesis. It is crucial to producing hardware designs with acceptable latency and throughput. However, it is a complex transformation involving aggressive scheduling strategies for high throughput and careful control generation to eliminate hazards. We present an equivalence checking approach for certifying synthesized hardware designs in the presence of pipelining transformations. Our approach works by (1) constructing a provably correct pipeline reference model from sequential specification, and (2) applying sequential equivalence checking between this reference model and synthesized RTL. We demonstrate the scalability of our approach on several synthesized designs from a commercial synthesis tool.

introduction Share on Introduction to special section on verification challenges in the concurrent world Authors: Sandip Ray University of Texas at Austin, TX University of Texas at Austin, TXView Profile , Jayanta Bhadra Freescale Semiconductor Inc., Austin, TX Freescale Semiconductor Inc., Austin, TXView Profile , Magdy S. Abadir Freescale Semiconductor Inc., Austin, TX Freescale Semiconductor Inc., Austin, TXView Profile , Li-C. Wang University of California at Santa Barbara, CA University of California at Santa Barbara, CAView Profile , Aarti Gupta NEC Laboratories America, Inc., Princeton, NJ NEC Laboratories America, Inc., Princeton, NJView Profile Authors Info & Claims ACM Transactions on Design Automation of Electronic SystemsVolume 17Issue 3June 2012 Article No.: 19pp 1–3https://doi.org/10.1145/2209291.2209292Published:05 July 2012Publication History 0citation172DownloadsMetricsTotal Citations0Total Downloads172Last 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 Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Behavioral synthesis is the compilation of an Electronic system-level (ESL) design into an RTL implementation. We present a suite of optimizations for equivalence checking of RTL generated through behavioral synthesis. The optimizations exploit the high-level structure of the ESL description to ameliorate verification complexity. Experiments on representative benchmarks indicate that the optimizations can handle equivalence checking of synthesized designs with tens of thousands of lines of RTL.

Recent years have seen continuing miniaturization of VLSI technologies, producing chips with very high transistor density. A consequence of this advancement, together with high computational demands of modern applications, is that hardware designs are rising in complexity to make use of all the available transistors. This makes it challenging to develop reliable hardware through hand-crafted RTL implementations. The problem is exacerbated with aggressive time-to-market requirements, leading to a design productivity gap. Electronic System Level (ESL) design is often seen as a solution to this gap: the idea is to raise the design abstraction by specifying a hardware design behaviorally with a high-level language (e.g., SystemC). High-level synthesis translates ESL specifications to RTL, through several inter-dependent transformations (e.g., compilation, scheduling, resource allocation, control synthesis, etc).

We present a framework for post-silicon analysis, that provides a formal, bidirectional communication with pre-silicon verification. We show how to exploit the framework to provide a formal guarantee on post-silicon verification accuracy under limited observability. In particular, we partition a pre-silicon assertion checker (with full observability) into (1) a limited-observability checker and (2) an in-silicon integrity unit. The composition of the two units is guaranteed to provide the same accuracy as a pre-silicon checker. We apply the framework in the verification of a cache system.

We present a method for verifying information flow properties of software programs using inductive assertions and theorem proving. Given a program annotated with information flow assertions at cutpoints, the method uses a theorem prover and operational semantics to generate and discharge verification conditions. This obviates the need to develop a verification condition generator (VCG) or a customized logic for information flow properties. The method is compositional: a subroutine needs to be analyzed once, rather than at each call site. The method is being mechanized in the ACL2 theorem prover, and we discuss initial results demonstrating its applicability.

Abstract We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.

We present a framework for formal verification of embedded custom memories. Memory verification is complicated by the difficulty in abstracting design parameters induced by the inherently analog nature of transistor-level designs. We develop behavioral formal models that specify a memory as a system of interacting state machines, and relate such models with an abstract read/write view of the memory via refinements. The operating constraints on the individual state machines can be validated by readily available data from analog simulations. The framework handles both static RAM (SRAM) and flash memories, and we show initial results demonstrating its applicability.