Abstract Convolutional Neural Networks (CNNs) proved highly successful in various applications, including image classification. CNNs demand a massive number of mathematical operations that represent a challenge in hardware implementation, especially for limited-resource devices or edge-computing devices. This paper presents Binary Weight CNN (BW-CNN) accelerator that can be deployed on Field Programmable Gate Array (FPGA). The BW-CNN provides efficient hardware optimization, by using 1-bit representation for weights and 2-bit representation for activations to minimize the model size and reduce the number of required multiplications. Moreover, binary weights enable the system to avoid memory access time bottleneck for reading the weights because they are saved on-chip. The BW-CNN supports hardware/software co-design approach for hardware acceleration. The proposed BW-CNN is implemented using Virtex UltraScale FPGA VCU108 Evaluation Kit. The BW-CNN is evaluated on the Modified National Institute of Standards and Technology (MNIST) dataset achieving 98.45% accuracy and consumes power of 3.599 W.

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.

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.