Contract-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.

Contract-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.

Contract-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.

Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derived automatically from its implementation. Our approach requires that the system implementation is specified in Lingua Franca (LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engine Uclid5 using the Z3 SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF V erifier and evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF V erifier correctly checks 21 out of 22 programs automatically.

The wavelength-routed optical network on chip (WRONoC) is a promising solution for signal transmission in modern System-on-Chip (SoC) designs. Previous works do not simultaneously handle all the following four main issues for WRONoCs: 1) correlations between the topological structure and physical layout; 2) tradeoffs between the maximum insertion loss and the number of wavelengths; 3) runtime scalability of wavelength assignment scheme; and 4) a fully automated flow to generate predictable designs. As a result, their insertion loss estimation is inaccurate, their wavelength assignment is inefficient, and thus, only suboptimal results are obtained. To remedy these disadvantages, we present a fully automated topological structure and a physical layout co-design flow with improved wavelength assignment schemes to minimize the maximum insertion loss and the laser power simultaneously with a significant speedup. The experimental results show that our co-design flow significantly outperforms state-of-the-art works in the maximum insertion loss, laser power, and runtimes.

As the VLSI technology continues to scale down, combined with increasing demands for large bandwidth and low-power consumption, the optical interconnections with wavelength-division multiplexing (WDM) become an attractive alternative for on-chip signal transmission. Previous WDM-aware optical routing works consist of three main drawbacks: they are based mainly on heuristics or restricted integer linear programming to handle optical routing, the addressed types of insertion loss, and WDM overheads are incomplete, and the crosstalk noise during concurrent signal transmission is neglected. As a result, no performance guarantees can be achieved on their WDM clustering results, the reliability of the optical network is impaired, and/or their computations are too time consuming. To remedy these disadvantages, we present a new WDM-aware optical routing flow to minimize the insertion loss, the WDM overheads, and the crosstalk noise with a significant speedup. In the proposed flow, the WDM-aware path clustering algorithm guarantees to find an optimal solution for 1-, 2-, and 3-path clustering and has the constant performance bound for most cases of 4-path clustering; the crosstalk-aware path assignment guarantees to minimize the number of crosstalk signal pairs within the given displacement bound. Experimental results based on the ISPD 2007 and 2019 contest benchmarks and a real optical design show that our optical router significantly outperforms published works in wirelength, insertion loss, wavelength power, crosstalk noise, and runtimes.

To improve manufacturability, dummy fill insertion is widely adopted for reducing the thickness variation after chemical mechanical polishing. However, inserted metal fills induce significant coupling to nearby signal nets, thus possibly incurring timing degradation. Existing timing-aware fill insertion strategies focus on optimizing induced coupling capacitance instead of resultant equivalent capacitance. Therefore, the impact on timing cannot be fully captured. In contrast, in this paper, we analyze equivalent capacitance friendly regions for dummy fills. The analysis can wisely guide dummy fill insertion to prevent unwanted and unnecessary increase in the resultant equivalent capacitance of timing critical nets. Experimental results based on the ICCAD 2018 CAD Contest benchmark suite show that our solution outperforms the contest winning teams and state-of-the-art work. Moreover, our analysis results are highly correlated to actual equivalent capacitance values and indeed provide accurate guidance for timing-aware dummy fill insertion.

The wavelength-routed optical network-on-chip (WRONoC) is a promising solution for signal transmission in modern system-on-chip (SoC) designs. Previous works do not handle three main issues for WRONoCs: correlations between the topological structure and physical layout, trade-offs between the maximum insertion loss and wavelength power, and a fully automated flow to generate predictable designs. As a result, the insertion loss estimation is inaccurate, and thus only suboptimal results are obtained. To remedy these disadvantages, we present a fully automated topological structure and physical layout codesign flow to minimize the maximum insertion loss and the wavelength power simultaneously with a significant speedup. Experimental results show that our codesign flow significantly outperforms state-of-the-art works in the maximum insertion loss, wavelength power, and runtimes.

As the VLSI technology continues to scale down, combined with increasing demands for large bandwidth and low-power consumption, the optical interconnections with Wavelength Division Multiplexing (WDM) become an attractive alternative for on-chip signal transmission. Previous WDM-aware optical routing works consist of two main drawbacks: they are based mainly on heuristics or restricted integer linear programming to handle optical routing, and the addressed types of transmission loss and WDM overheads are incomplete. As a result, no performance guarantees can be achieved on their WDM clustering results, and/or their computations are too time-consuming. To remedy these disadvantages, we present a polynomial-time provably good WDM-aware clustering algorithm and a new WDM-aware optical routing flow to minimize the transmission loss and the WDM overheads with a significant speedup. The proposed WDM-aware clustering algorithm guarantees to find an optimal solution for 1-, 2-, and 3-path clustering, and has the constant performance bound 3 for most cases of 4-path clustering. Experimental results based on the ISPD 2007 and 2019 contest benchmarks and a real optical design show that our optical router significantly outperforms published works in wirelength, transmission loss, wavelength power, and runtimes.