Search

Reduction to satisfiability of constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. Current CHC-based methods, however, do not work very well for pointer-manipulating programs, especially those with dynamic memory allocation. This article presents a novel reduction of pointer-manipulating Rust programs into CHCs, which clears away pointers and memory states by leveraging Rust’s guarantees on permission. We formalize our reduction for a simplified core of Rust and prove its soundness and completeness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.

A wireless inductive coupling ThruChip Interface (TCI) is a flexible system-in-package (SiP) technique which enables to build a powerful interconnection network between stacked chips. For easy use of TCI, intellectual properties (IPs) are developed, and interconnection networks which can make the use of IPs are proposed and evaluated based on the real chip implementation. The new proposed elevator network which uses piggyback of the credit packets outperforms the ring network used in the first prototype by 28%-59% in terms of throughput. The performance overhead by the piggyback control is less than 3%-4%.

This paper explores the grain of domain size of an energy efficient coarse grained reconfigurable array called CMA (Cool Mega Array). By using Genetic Algorithm based body bias assignment method, the leakage reduction of various grain size was evaluated. As a result, a domain with 2×1 PEs achieved about 40% power reduction with a 6% area overhead.