Abstract In modern chip designs, shared resources are used extensively. Arbiters usage is crucial to settle conflicts when multiple requests compete for these shared resources. Making sure these arbiter circuits work correctly is vital not just for their proper functionality, but also for security reasons. The work in this paper introduces a method based on formal verification to thoroughly assess the proper functional aspects of various arbiter setups. This is achieved through SystemVerilog assertions and model checking. Additionally, we explore a non-invasive method for the modeling and insertion of different types of hardware Trojans. These Trojans, with their unique triggers and payloads, are modeled formally without the need for any alterations to the actual circuit. The results provide a detailed analysis of the cost involved in running the formal verification environment on versions of arbiters that are free from Trojans. This analysis is carried out using Questa PropCheck formal analysis tool, which offers valuable insights into the time and memory resources required. Furthermore, the results highlights how the formally modeled and inserted Trojans interfere with hold criteria of the arbiters’ properties, where at least a single property fires due to the inserted Trojan. This work can be extended to be a generic approach with the potential to validate both the proper operation and security aspects of complex systems.

A wide variety of embedded instruments are increasingly integrated within modern System-on-Chips (SoCs) for the purpose of monitoring, debugging, and testing. Integrating this heterogeneous set of embedded instruments within the same chip necessitates having an efficient access network. Such a network should ensure minimal access time to the embedded instruments. The IJTAG standard was introduced as an efficient access methodology for instruments embedded in chips. The required configurations to access the desired instruments are generated in a process called pattern retargeting. For optimal retargeting, it is important to minimize the time taken to find the right configuration vectors as well as the time to access the desired instruments. In this work, we express the two execution times using the term Dynamic Access Time (DAT). This work proposes an adaptive retargeting model based on the Boolean Satisfiability Problem (SAT) that properly fits any arbitrary IJTAG network. The proposed model should provide substantial improvement, especially for runtime applications requiring dynamic retargeting, such as debugging operations. To assess the effectiveness of our proposed model, a comparison between state-of-the-art retargeting techniques and our work is performed. The results show an improvement in retargeting time of 60%, on average, compared to previous SAT-based retargeting approaches.

Due to the scale of modern systems, pre-silicon security has become a major concern for design and verification engineers. In this paper, we propose a formal verification framework for the verification of different arbiter circuits with different protocols and sizes using SystemVerilog Assertions (SVA). We also propose a formal way of the modeling and insertion of hardware Trojans of different trigger and payload types without applying any modifications to the Design Under Test (DUT). The obtained results show the formal analysis statistics in terms of time and memory for Trojan-free designs for a set of all-proven properties. It also shows how Trojan insertion affects the pass-fail criteria of the formal properties, where at least a single property fails due to the inserted Trojan. The proposed work can be generalized to verify the correct functionality and security of an arbiter circuit placed within any complex system.

A growing number of embedded instruments is being integrated into System-on-Chips for testing, monitoring, and several other purposes. To standardize their access protocols, the IEEE 1687 (IJTAG) standard has defined a flexible network infrastructure. Finding the shortest path in such networks requires a comprehensive search over a solution space, bounded by a limited number of time frames. This bound must be selected carefully, as it can neither be too large (to avoid unnecessary long execution time) nor too small (to avoid missing the optimal solution). Previous work was not efficiently applicable to all segments of IJTAG networks, with some providing unrealistic bounds and others having scope limitations or scalability issues. In this work, we present a new methodology for computing the upper-bound on the number of time frames using the Boolean Satisfiability Problem (SAT). Our proposed technique can also be customized to perfectly adapt to instruments access procedures, which in turn increases efficiency by reducing the time spent searching for required configurations. Results show the effectiveness of our work in computing the upper-bound for irregular benchmarks that are not constrained by a specific network design. This is achieved with a controlled increase in execution time, in contrast to previous work.

The IEEE 1687 standard introduced a large design space of compliant networks for accessing embedded instruments. Such networks could grow in their structural complexity and inter-component temporal dependencies. Scan pattern retargeting is defined as the procedure of translating an instrument-level pattern to several network-level ones. Pattern retargeting could become computationally intensive with the increase of structural and temporal dependencies. Structured pattern retargeting was previously introduced as a formal and light-weight pattern retargeting methodology for arbitrary IEEE 1687 networks. In this work, we present a dedicated structured retargeting method for hierarchical IEEE 1687 networks. The proposed method significantly reduces the retargeting time for pure hierarchical networks compared to the general one, while resulting in the same network access time. The retargeting time is of a special importance in the case of on-chip retargeting, which is used for on-line monitoring using IEEE 1687 networks.

Integrated framework to simulate electronic system (including digital and analog devices) with the mechanical parts of a heterogeneous automotive system is presented. The electronic system, consisting of many Electronic Control Units (ECUs), is modeled to simulate the mechatronic system functionality. The recently developed Functional Mock-up standard approach is used to have a model for a complex cyber-physical automotive system. The framework simulates real system including the Hardware (HW) and the Software (SW) to run on the ECUs. It allows Co-development of the automotive system SW and HW while the mechanical system is in the loop. Hardware and Software debugging is demonstrated using the developed methodology. The development cycle for the automotive mechatronic system could be greatly shortened using the proposed framework.

The ISO 26262 defines discrete Automotive Safety Integrity Levels (ASILs) to enforce functional safety. Each component in the automotive system under development must have an associated ASIL. Higher ASIL implies more development cost and effort. ASIL decomposition allows reducing ASIL allocated to components whose joint failure is the only cause for the violation of a safety goal. Fault trees are widely used in the safety analysis process and hence in the ASIL allocation. In this paper, we present a new approach for solving the ASIL decomposition problem using Satisfiability Modulo Theories (SMT). The fault tree structure is fully represented in SMT. Compared to other approaches for ASIL decomposition; our approach eliminates the need of finding the Minimal Cut Set (MCS) of the fault tree. Moreover, it does not require assigning a numerical cost value for each ASIL. Recent emerging trend in powerful SMT solvers for solving objective functions is utilized to find the optimal ASIL decomposition.

A multi-processor system is an integrated circuit containing multiple processor cores that implements most of the functionality of a complex electronic system and some other components like FPGA/ASIC on a single chip. In this paper, we present a novel approach to synthesize multi-core system architectures from Task Precedence Graphs (TPG) models. The front end engine applies efficient algorithm for scheduling and communication contention resolving to obtain the optimal multi-core system architecture in terms of number of processor cores, number of busses, task-to-processor/channel-to-bus mapping, optimal schedule, and hardware-software (HW-SW) partition. The scheduling and mapping algorithms produce the optimality of mapping tasks onto cores. The partitioning technique reduces the overall execution time and number of buses among the cores. The back end engine generates a SystemC simulation model using a well-known commercial tool model generation library. The viability and potential of the proposed algorithms are demonstrated by a case study and extensive experimental results to conclude that the proposed approach is an efficient scheme to obtain the optimality of scheduling, mapping and partitioning with hard and large task graph problems.

Several approaches have been proposed to accelerate the NP-complete Boolean Satisfiability problem (SAT) using reconfigurable computing. In this paper, we present a five-stage pipelined SAT solver. SAT solving is broken into five stages: variable decision, variable effect fetch, clause evaluation, conflict detection, and conflict analysis. The solver performs a novel search algorithm combining state-of-the-art SAT solvers advanced techniques: non-chronological backjumping, dynamic backtracking and learning without explicit traversal of implication graph. SAT instance information is stored into FPGA block RAMs avoiding synthesizing overhead for each instance. The proposed solver achieves up to 70× speedup over other hardware SAT solvers with 200× less resource utilization.

The Boolean Satisfiability problem (SAT) is an NP-complete problem so software SAT’s solving algorithm execution time influences the performance of SAT-based CAD tools. In this paper, we present a new approach for implementing conflict analysis based on a conflicting variables accumulator and priority encoder to determine backtrack level. Using this approach, we implement an FPGA-based SAT solver performing depth-first search with conflict directed nonchronological backtracking. We compare our SAT solver with other SAT solvers through instances from DIMACS benchmarks suite.

Several approaches have been proposed to accelerate the NP-complete Boolean satisfiability problem (SAT) using reconfigurable computing. We present an FPGA based clause evaluator, where each clause is modeled as a shift register that is either right shifted, left shifted, or standstill according to whether the current assigned variable value satisfy, unsatisfy, or does not effect the clause, respectively. For a given problem instance, the effect of the value of each of its variables on its SAT formula is loaded in the FPGA on-chip memory. This results in less configuration effort and fewer hardware resources than other available SAT solvers. Also, we present a new approach for implementing conflict analysis based on a conflicting variables accumulator and priority encoder to determine backtrack level. Using these two new ideas, we implement an FPGA based SAT solver performing depth-first search with non-chronological conflict directed backtracking. We compare our SAT solver with other solvers through instances from DIMACS benchmarks suite