A Novel low power 2-D to 3-D Array Priority Encoder using Split-Logic Technique for Data Path Applications

In this work, an ascendable low power 64-bit priority encoder is designed using a two-directional array to three-directional array conversion, and Split-logic technique and 6-bit is obtained as the output. By using this method, the high performance priority encoder can be achieved. In the conventional priority encoder, a single bit is set as an input, but for a priority encoder with 3-Darray, every input are specified in the matrix form. The I-bit input file is split hooked on M × N bits, similar to 2-D Matrix. In priority encoder with 3-Darray, three directional output comes out, unlike traditional priority encoder, where the output is received from one direction. The development can be achieved by implementing the two-directional array to three-directional array technique. Simulation results show that the proposed 2-D and 3-D priority encoder consumes 0.087039mW and 0.184014mW which is less when compared with the conventional priority encoder. The priority encoders are simulated and synthesized using VHDL in Xilinx Vivado version 2019.2 and the Oasys synthesis tool.

Synbit: synthesizing bidirectional programs using unidirectional sketches

We propose a technique for synthesizing bidirectional programs from the corresponding unidirectional code plus a few input/output examples. The core ideas are: (1) constructing a sketch using the given unidirectional program as a specification, and (2) filling the sketch in a modular fashion by exploiting the properties of bidirectional programs. These ideas are enabled by our choice of programming language, HOBiT, which is specifically designed to maintain the unidirectional program structure in bidirectional programming, and keep the parts that control bidirectional behavior modular. To evaluate our approach, we implemented it in a tool called Synbit and used it to generate bidirectional programs for intricate microbenchmarks, as well as for a few larger, more realistic problems. We also compared Synbit to a state-of-the-art unidirectional synthesis tool on the task of synthesizing backward computations.

Hardware Context Switch-based Cryptographic Accelerator for Handling Multiple Streams

The confidentiality and integrity of a stream has become one of the biggest issues in telecommunication. The best available algorithm handling the confidentiality of a data stream is the symmetric key block cipher combined with a chaining mode of operation such as cipher block chaining (CBC) or counter mode (CTR). This scheme is difficult to accelerate using hardware when multiple streams coexist. This is caused by the computation time requirement and mainly by management of the streams. In most accelerators, computation is treated at the block-level rather than as a stream, making the management of multiple streams complex. This article presents a solution combining CBC and CTR modes of operation with a hardware context switching. The hardware context switching allows the accelerator to treat the data as a stream. Each stream can have different parameters: key, initialization value, state of counter. Stream switching was managed by the hardware context switching mechanism. A high-level synthesis tool was used to generate the context switching circuit. The scheme was tested on three cryptographic algorithms: AES, DES, and BC3. The hardware context switching allowed the software to manage multiple streams easily, efficiently, and rapidly. The software was freed of the task of managing the stream state. Compared to the original algorithm, about 18%–38% additional logic elements were required to implement the CBC or CTR mode and the additional circuits to support context switching. Using this method, the performance overhead when treating multiple streams was low, and the performance was comparable to that of existing hardware accelerators not supporting multiple streams.

Vacuity in synthesis

In reactive synthesis, one begins with a temporal specification $$\varphi $$ φ , and automatically synthesizes a system $$M$$ M such that $$M\models \varphi $$ M ⊧ φ . As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies $$\varphi $$ φ non-vacuously, then M is likely to be closer to the user’s intent, because it satisfies $$\varphi $$ φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

The Notification Oriented Paradigm Language to Digital Hardware as an Intuitive High-level Synthesis Tool

The parallelism allowed by FPGAs has attracted attention for knowing applications that need processing power. However, the need for specific and very technical development language has not stimulate its broad use. As an alternative, there are High-level Synthesis Languages (HSL), which allow less complicated FPGA use. However, they do not tend to take full advantage of the FPGA technology. Therefore, another alternative was developed, based on the Notification Oriented Paradigm (NOP), called NOP for Digital Hardware (NOP-DH). NOP allows development in high level with its rule-oriented language called NOPL. Its entity decoupling, parallelism, and redundancy avoidance are useful for best performance. In turn, the NOP-DH brings NOP for the FPGA context with the benefits observed in software but enhanced by hardware nature. This paper reviews the NOPL for NOP-DH (NOPL-DH) that aims high level programming for FPGA. The paper proposes the NOPL-DH test by independent developers, by developing a monitoring device for a box transporting bidirectional conveyer. As a result, NOPL-DH allowed high-level development under the NOP-DH structure in an FPGA, without the need for technical knowledge and, still, maintaining and exploring the NOP properties in FPGA

A Framework for Validation of Synthesized MicroElectrode Dot Array Actuations for Digital Microfluidic Biochips

Digital Microfluidics is an emerging technology for automating laboratory procedures in biochemistry. With more and more complex biochemical protocols getting mapped to biochip devices and microfluidics receiving a wide adoption, it is becoming indispensable to develop automated tools and synthesis platforms that can enable a smooth transformation from complex cumbersome benchtop laboratory procedures to biochip execution. Given an informal/semi-formal assay description and a target microfluidic grid architecture on which the assay has to be implemented, a synthesis tool typically translates the high-level assay operations to low-level actuation sequences that can drive the assay realization on the grid. With more and more complex biochemical assay protocols being taken up for synthesis and biochips supporting a wider variety of operations (e.g., MicroElectrode Dot Arrays (MEDAs)), the task of assay synthesis is getting intricately complex. Errors in the synthesized assay descriptions may have undesirable consequences in assay operations, leading to unacceptable outcomes after execution on the biochips. In this work, we focus on the challenge of examining the correctness of synthesized protocol descriptions, before they are taken up for realization on a microfluidic biochip. In particular, we take up a protocol description synthesized for a MEDA biochip and adopt a formal analysis method to derive correctness proofs or a violation thereof, pointing to the exact operation in the erroneous translation. We present experimental results on a few bioassay protocols and show the utility of our framework for verifiable protocol synthesis.