Experimental demonstration of an integrated on-chip p-bit core utilizing stochastic Magnetic Tunnel Junctions and 2D-MoS2 FETs
Authors:
John Daniel,
Zheng Sun,
Xuejian Zhang,
Yuanqiu Tan,
Neil Dilley,
Zhihong Chen,
Joerg Appenzeller
Abstract:
Probabilistic computing is a novel computing scheme that offers a more efficient approach than conventional CMOS-based logic in a variety of applications ranging from optimization to Bayesian inference, and invertible Boolean logic. The probabilistic-bit (or p-bit, the base unit of probabilistic computing) is a naturally fluctuating entity that requires tunable stochasticity; by coupling low-barri…
▽ More
Probabilistic computing is a novel computing scheme that offers a more efficient approach than conventional CMOS-based logic in a variety of applications ranging from optimization to Bayesian inference, and invertible Boolean logic. The probabilistic-bit (or p-bit, the base unit of probabilistic computing) is a naturally fluctuating entity that requires tunable stochasticity; by coupling low-barrier stochastic Magnetic Tunnel Junctions (MTJs) with a transistor circuit, a compact implementation is achieved. In this work, through integrating stochastic MTJs with 2D-MoS$_{2}$ FETs, the first on-chip realization of a key p-bit building block displaying voltage-controllable stochasticity is demonstrated. In addition, supported by circuit simulations, this work provides a careful analysis of the three transistor-one magnetic tunnel junction (3T-1MTJ) p-bit design, evaluating how the characteristics of each component influence the overall p-bit output. This understanding of the interplay between the characteristics of the transistors and the MTJ is vital for the construction of a fully functioning p-bit, making the design rules presented in this article key for future experimental implementations of scaled on-chip p-bit networks.
△ Less
Submitted 16 October, 2023; v1 submitted 21 August, 2023;
originally announced August 2023.
Bounded verification of message-passing concurrency in Go using Promela and Spin
Authors:
Nicolas Dilley,
Julien Lange
Abstract:
This paper describes a static verification framework for the message-passing fragment of the Go programming language. Our framework extracts models that over-approximate the message-passing behaviour of a program. These models, or behavioural types, are encoded in Promela, hence can be efficiently verified with Spin. We improve on previous works by verifying programs that include communication-rel…
▽ More
This paper describes a static verification framework for the message-passing fragment of the Go programming language. Our framework extracts models that over-approximate the message-passing behaviour of a program. These models, or behavioural types, are encoded in Promela, hence can be efficiently verified with Spin. We improve on previous works by verifying programs that include communication-related parameters that are unknown at compile-time, i.e., programs that spawn a parameterised number of threads or that create channels with a parameterised capacity. These programs are checked via a bounded verification approach with bounds provided by the user.
△ Less
Submitted 2 April, 2020;
originally announced April 2020.
