The growing complexity of modern digital systems and the increasing volumes of code written in hardware description languages demand effective tools for early error detection in the development of digital ASICs. To facilitate timely error detection, rule sets are created to regulate hardware descriptions. These rule sets contain a collection of rules that describe inaccuracies, errors, and the consequences of their violation. This paper discusses a list of rules developed based on the experience of engineers using the SystemVerilog language and presents the SVAN static analysis system, designed for SystemVerilog and tailored to the specifics of hardware descriptions. The proposed system provides full support for the SystemVerilog IEEE 1800-2017 standard and offers capabilities for analyzing descriptions for structural and semantic errors.
The paper describes a way of organizing static analysis on abstract syntax trees (AST) widely used for finding coding errors as well as errors that do not require deep understanding of program semantics. For most known types of errors, a formalization is proposed that is based on finite automata over trees (FATs), similar to NFAs and DFAs for regular languages over an alphabet. In contrast to the theory of FATs developed for alphabets with bounded arity, which in practice fixes the number of children for each node type, the case of a finite number of children without a priori bound is considered. Nondeterministic and deterministic FAT are described, their equivalence is shown, the closure of regular languages over trees with respect to union and intersection is shown, and the linear complexity of the FAT tree recognition problem is proven. For the AST analysis algorithms not covered by regular languages over trees, context-free languages are considered.
The work is devoted to the analysis of the hydrodynamic model of the Tesla valve, which allows to regulate the flow of liquid in the design of a microfluidic chip. When modelling fluid motion in complex Tesla valves consisting of several loops, one often resorts to analyzing a single loop and further extrapolating the results to the entire valve. To confirm or refute the validity of this method, valves consisting of one and eight loops are analyzed in the work. The resulting pressure difference and diodicity were studied. Based on the obtained data, it was revealed that the hydrodynamics of the Tesla valve is nonlinear and does not correctly generalize the results obtained for one loop to valves consisting of a larger number of loops.
Nowadays, programming languages that use language virtual machines (VMs) in their infrastructure are very popular, which stimulates the development of this technology. Developing a language VM is a complex process, during which errors can be introduced into the designed system. To ensure the quality of the VM implementation, the development process includes a testing stage. During testing, it is necessary to answer two main questions: how to create test programs and how to check the result of their execution. The article presents a method for functional testing of language VMs based on formal specifications of the instruction set architecture (ISA). The work describes the implementation of the proposed approach. Based on the VM documentation, the ISA is specified using the architecture description language. An executable model is built based on the ISA specification. Test templates, which are parameterized descriptions of test programs, are used to automate the creation of test programs. When creating test templates, a special domain-specific language is used, which allows you to specify various generation techniques and use the VM bytecode obtained from formal specifications. In the presented method, test templates can be described manually, generated automatically in accordance with the target criterion, or obtained from third-party generators. Based on the test templates and the executable model, test programs are generated in bytecode aimed at checking a certain functionality or properties of the system under test. Bytecode is a natural language for the VM and allows you to affect all of its functionality. The test program is translated into a binary program and executed on the VM. During the program execution, an execution trace is collected on the VM. A trace adapter is created to analyze the execution trace. A test oracle is built based on the executable model and the trace adapter. The oracle checks the test results by comparing the execution trace with the results of executing the binary program on the executable model. The method is implemented in the MicroTESK tool version 2.6 and was used to test the Ark (Panda) VM.
The development of matrix extensions of processor architectures, as well as the implementation of these extensions in specialized AI processors, can significantly improve the efficiency of artificial neural networks. The paper provides an overview of the basic functionality of some popular matrix extensions of processor architectures, in particular, ARM SME, RISC-V IME, RISC-V AME extensions, as well as the DaVinci processor architecture. As a result of the analysis, a model of an abstract matrix processor was proposed. This model reflects the features of modern processor architectures supporting matrix extensions. For the introduced model of the matrix processor, a heterogeneous matrix intermediate representation was developed, which can be used to build compilers for neural networks. The proposed intermediate representation was implemented in the MLIR infrastructure as a heteroMx dialect. The paper also describes an approach to building an AI compiler using the heteroMx dialect. The developed intermediate representation can be adapted or specified for other matrix processor architectures.
In this paper, we examine shared memory concurrent programs and errors occurring in them, specifically data races. We design a test automation framework to develop data race revealing testing scenarios by analogy to test automation frameworks for sequential programs. The main problem complicating development of testing scenarios is the nondeterministic nature of multithreaded program executions. To provide repeatable testing scenarios we define a notion of synchronization points in the source code of the computer program where a test regulates execution of parallel threads with synchronization actions. Tests being developed with our test automation framework can be executed automatically and can be used for regression testing.
Due to the need to increase labor productivity when analyzing (marking up) the results of an automated vulnerability search in programs conducted using SAST (Static Application Security Testing) tool, there is a problem of a shortage in the market of highly qualified analysts to mark up the results. The paper describes a developed technique for finding vulnerabilities in software written in several programming languages (C, C++, Java, Python, Go). During its development, an analysis of all automatically detectable detectors in programs in these languages and elements of their structures to be analyzed was carried out. The detectors are ordered according to the classification of the regulator. The application of the methodology allows reducing the qualification requirements for analysts conducting markup and training such specialists in developing companies.
The paper is devoted to the description of the process of developing a new CAD architecture for high‑level modeling of NoC, as well as the remote flow of NoC design. The paper analyzes the main stages of NoC design and demonstrates the high importance of high-level modeling and its impact on the entire design process. Also, the possibility of conducting high-level modeling in a remote format using the client server architecture of the CAD is considered. The process of remote design of NoC using the proposed CAD system and remote testbed with FPGA debug boards is demonstrated.
This paper presents a deep neural network architecture for automatic phoneme recognition in speech signals. The proposed model combines convolutional and recurrent layers, as well as an attention mechanism enriched with reference values of vowel formant frequencies. This allows the model to effectively extract local and global acoustic features necessary for accurate phoneme sequence recognition. Particular attention is paid to the problem of imbalanced phoneme frequency in the training dataset and ways to overcome it, such as data augmentation and the use of a weighted loss function. The reported results demonstrate the viability of the proposed approach, but also indicate the need for further model refinement to achieve higher accuracy and recall in the speech recognition task.
We present our experience of organizing the second contest in formal program verification for young engineers, researchers, and students from Russia. The contest was held in conjunction with the Workshop on Program Semantics, Specification, and Verification (PSSV) in Innopolis in October 2024. The contest format was close to the format of the so-called hackathons. Participants were asked to select and solve any of 5 verification problems using pre-defined model checking and deductive verification tools (Frama-C, Coq, C-lightVer, SPIN, TLC). We discuss the issues of organizing of the contest, the problems set, lessons learned from solutions submitted by contestants, and the overall feedback from the participants.
This research paper focuses on the use of artificial intelligence technologies for the Rorschach test. Machine learning techniques are considered. Both of these methods are used for multi-class classification of response categories. The paper describes the algorithms of machine learning and deep learning methods for interpreting the results, the algorithm for scoring one of the categories and the final test result in the web interface for the user. The application of artificial intelligence for projective testing techniques, on the example of the Rorschach test, opens new opportunities for self-diagnosis and therapy.
Nowadays the task of building digital twins of various natural and technical objects is an urgent task. The paper considers the possibilities of open source software for the development of digital twins of soil processes. Cloud platform for scientific research can be designed and created on the basis of hardware and software complex, which includes such components as servers, data storage system, network equipment, system software stack, virtual machines, microservices and other elements. The cloud platform can act as the main platform for digital twin development projects. Meteorological data, data on digital terrain relief, data on physical and chemical composition of soil, data on agricultural crops, synthetic data can be used as input data for building a digital twin of soil fields. In the article the possibilities of open-source software packages ParFlow, OpenFOAM, Paraview for modeling of soil processes using Richards equation for single-phase medium are considered. Physical modeling was carried out for cases of model soil fields with given permeability and porosity of the medium. As a result of the calculation, the fields of moisture saturation, hydrostatic head, and moisture velocity were obtained. In one of the modeling problems the influence of well presence on the pressure field was also investigated. The basic calculation grid included 288,000 calculation cells. Typical calculations were performed on the high-performance cluster of ISP RAS. One typical calculation was run on 12 cores and took about 20 minutes. Visualization of the calculation results was performed in the Paraview package using filter technology and software scripts in the Python programming language.
A modification of the immersed boundary method LS-STAG with level functions has been developed to simulate flows of non-Newtonian viscous fluids. The viscosity of these fluids is completely determined by the intensity of the strain rate tensor at each point at any time. The LS-STAG method modification was previously developed for another class of non-Newtonian fluids (viscoelastic fluids). The modification demonstrated high accuracy even for viscoelactic flows characterized by high values of the Weissenberg number. Therefore, it is of interest to generalize the LS-STAG method for non-Newtonian viscous fluids. Note that although the LS-STAG method can be successfully used to simulate flows with moving immersed boundaries, this paper focuses only on flows with fixed ones. The developed numerical method can be used both for viscoplastic fluids and for generalized Newtonian fluids that do not have a yield point. For viscoplastic fluids, the Ofoli-Morgan-Steffe, Mizrahi-Burk, Casson, and Herschel-Bulkley models used with the Bercovier-Engelmann and Papanastasiou regularization models are considered, and for fluids that do not have a yield point, the Ellis, Cross, Carreau, Yasuda (Carreau-Yasuda) models, as well as the Ostwald-de Waele power model are considered. To verify the numerical method developed and implemented in the author's software package, a well-studied problem of power-law flow past a stationary circular airfoil was used at different values of the Reynolds number and flow index. The obtained results are in good agreement with the known in the literature computational data of other researchers. In the future, it is planned to generalize the developed modification of the LS-STAG method for non-Newtonian viscous fluids simulation for the case of moving immersed boundaries.
ISSN 2220-6426 (Online)