The advancement of Large Language Models (LLM) has also resulted in an equivalent proliferation in its applications. Software design, being one, has gained tremendous benefits in using LLMs as an interface component that extends fixed user stories. However, inclusion of LLM-based AI agents in software design often poses unexpected challenges, especially in the estimation of development efforts. Through the example of UI-based user stories, we provide a comparison against traditional methods and propose a new way to enhance specifications of natural language-based questions that allows for the estimation of development effort by taking into account data sources, interfaces and algorithms.
Property Specification Language (PSL) is a form of temporal logic that has been mainly used in discrete domains (e.g. formal hardware verification). In this paper, we show that by merging machine learning techniques with PSL monitors, we can extend PSL to work on continuous domains. We apply this technique in machine learning-based anomaly detection to analyze scenarios of real-time streaming events from continuous variables in order to detect abnormal behaviors of a system. By using machine learning with formal models, we leverage the strengths of both machine learning methods and formal semantics of time. On one hand, machine learning techniques can produce distributions on continuous variables, where abnormalities can be captured as deviations from the distributions. On the other hand, formal methods can characterize discrete temporal behaviors and relations that cannot be easily learned by machine learning techniques. Interestingly, the anomalies detected by machine learning and the underlying time representation used are discrete events. We implemented a temporal monitoring package (TEF) that operates in conjunction with normal data science packages for anomaly detection machine learning systems, and we show that TEF can be used to perform accurate interpretation of temporal correlation between events.
Analysis of large observational data sets generated by a reactive system is a common challenge in debugging system failures and determining their root cause. One of the major problems is that these observational data suffer from survivorship bias. Examples include analyzing traffic logs from networks, and simulation logs from circuit design. In such applications, users want to detect non-spurious correlations from observational data and obtain actionable insights about them. In this paper, we introduce log to Neuro-symbolic (Log2NS), a framework that combines probabilistic analysis from machine learning (ML) techniques on observational data with certainties derived from symbolic reasoning on an underlying formal model. We apply the proposed framework to network traffic debugging by employing the following steps. To detect patterns in network logs, we first generate global embedding vector representations of entities such as IP addresses, ports, and applications. Next, we represent large log flow entries as clusters that make it easier for the user to visualize and detect interesting scenarios that will be further analyzed. To generalize these patterns, Log2NS provides an ability to query from static logs and correlation engines for positive instances, as well as formal reasoning for negative and unseen instances. By combining the strengths of deep learning and symbolic methods, Log2NS provides a very powerful reasoning and debugging tool for log-based data. Empirical evaluations on a real internal data set demonstrate the capabilities of Log2NS.
In this paper, we introduce the QKeras library, an extension of the Keras library allowing for the creation of heterogeneously quantized versions of deep neural network models, through drop-in replacement of Keras layers. These models are trained quantization-aware, where the user can trade off model area or energy consumption by accuracy. We demonstrate how the reduction of numerical precision, through quantization-aware training, significantly reduces resource consumption while retaining high accuracy when implemented on FPGA hardware. Together with the hls4ml library, this allows for a fully automated deployment of quantized Keras models on chip, crucial for ultra low-latency inference. As a benchmark problem, we consider a classification task for the triggering of events in proton-proton collisions at the CERN Large Hadron Collider, where a latency of ${\mathcal O}(1)~\mu$s is required.
Practical machine learning applications involving time series data, such as firewall log analysis to proactively detect anomalous behavior, are concerned with real time analysis of streaming data. Consequently, we need to update the ML models as the statistical characteristics of such data may shift frequently with time. One alternative explored in the literature is to retrain models with updated data whenever the models accuracy is observed to degrade. However, these methods rely on near real time availability of ground truth, which is rarely fulfilled. Further, in applications with seasonal data, temporal concept drift is confounded by seasonal variation. In this work, we propose an approach called Unsupervised Temporal Drift Detector or UTDD to flexibly account for seasonal variation, efficiently detect temporal concept drift in time series data in the absence of ground truth, and subsequently adapt our ML models to concept drift for better generalization.
Anomaly detection for time-series data becomes an essential task for many data-driven applications fueled with an abundance of data and out-of-the-box machine-learning algorithms. In many real-world settings, developing a reliable anomaly model is highly challenging due to insufficient anomaly labels and the prohibitively expensive cost of obtaining anomaly examples. It imposes a significant bottleneck to evaluate model quality for model selection and parameter tuning reliably. As a result, many existing anomaly detection algorithms fail to show their promised performance after deployment. In this paper, we propose LaF-AD, a novel anomaly detection algorithm with label-free model selection for unlabeled times-series data. Our proposed algorithm performs a fully unsupervised ensemble learning across a large number of candidate parametric models. We develop a model variance metric that quantifies the sensitivity of anomaly probability with a bootstrapping method. Then it makes a collective decision for anomaly events by model learners using the model variance. Our algorithm is easily parallelizable, more robust for ill-conditioned and seasonal data, and highly scalable for a large number of anomaly models. We evaluate our algorithm against other state-of-the-art methods on a synthetic domain and a benchmark public data set.
The ever-growing computational demands of increasingly complex machine learning models frequently necessitate the use of powerful cloud-based infrastructure for their training. Binary neural networks are known to be promising candidates for on-device inference due to their extreme compute and memory savings over higher-precision alternatives. However, their existing training methods require the concurrent storage of high-precision activations for all layers, generally making learning on memory-constrained devices infeasible. In this article, we demonstrate that the backward propagation operations needed for binary neural network training are strongly robust to quantization, thereby making on-the-edge learning with modern models a practical proposition. We introduce a low-cost binary neural network training strategy exhibiting sizable memory footprint reductions while inducing little to no accuracy loss vs Courbariaux & Bengio’s standard approach. These decreases are primarily enabled through the retention of activations exclusively in binary format. Against the latter algorithm, our drop-in replacement sees memory requirement reductions of 3–5×, while reaching similar test accuracy (± 2 pp) in comparable time, across a range of small-scale models trained to classify popular datasets. We also demonstrate from-scratch ImageNet training of binarized ResNet-18, achieving a 3.78× memory reduction. Our work is open-source, and includes the Raspberry Pi-targeted prototype we used to verify our modeled memory decreases and capture the associated energy drops. Such savings will allow for unnecessary cloud offloading to be avoided, reducing latency, increasing energy efficiency, and safeguarding end-user privacy.
Functional verification is “the” major design-phase bottleneck for silicon productivity. Since functional verification is an NP-complete problem, it relies on a large number of heuristics with associated parameters (engines). With the advent of parallel processing, formal verification can be optimized by selecting the best n engines to run in parallel, increasing the chance of reaching successful termination of the verification task. In this paper, we will present a methodology to build engine estimators based on structural metrics and to select n engines to run in parallel. The methodology considers both engines’ estimated performance and engines’ correlation. Results confirmed that the methodology can be a very quick selection mechanism for parallelization of engines in order to increase the chance of running the best engines to solve the problem.
Even with simulation and formal verification techniques, some bugs reach the silicon, thus, nowadays post-silicon debug techniques are vital for the fabrication of reliable integrated circuits. One approach used is the assertionbased design, in which an assertion processor (AP) can be employed to monitor synthesized property checkers. To reduce area overhead and provide more flexibility through the project stages, in this paper an external AP is implemented using a softcore processor and embedded software. A case study of the architecture using a MIPS32 based processor is also discussed. The area of the synthesized processor with the structure needed to connect itself to the external AP presented an increased of only 0.5%. Furthermore, the implementation costs of the proposed architecture are analysed.
Verification is the most challenging and time consuming stage in the integrated circuit development cycle. As designs complexities double every two years, novel verification methodologies are needed. We propose an algorithm that dynamically builds and updates an HDL module error proneness list. This list can be used to assist the development team to allocate resources during verification stage. The algorithm is build up using the idea that problematic modules usually hide many uncovered errors. Thus, our algorithm caches the most frequently modified and fixed modules. In an academic experiment composed by 17 modules, using a cache of size 3, we were able to correctly predict almost 80% of the faults occurrences.
Software evolution is the term used to describe the process of developing and updating software systems. Software repositories such as versioning systems and bug tracking systems are used to manage the evolution of software projects. The mining of this information is used to support predictions and improve design and reuse. Integrated circuit development can also benefit from these techniques. Nowadays, both software and hardware development use repositories and bug tracking systems. There are many hardware open source projects such as SUN's OpenSparc and designs at Opencores.org. We propose a methodology to track specific HDL metrics in order to improve design quality. Our results present a case study that correlates HDL metrics and bug proneness of Verilog HDL modules. We also present EyesOn, an open source framework designed to automate historical and complexity metrics tracking of HDL projects.
Verification is one of the most critical stages in integrated circuit development. Given the current market conditions, a wise manner to improve verification results would be concentrating resources in error-prone modules. In this paper a novel method of attaching information to commit messages is introduced. Through the use of a simple and parseable language, important and more accurate statistics can be retrieved. Tools were developed in order to make commits faster and prevent erroneous data analysis.
The latest advancements in the commercial formal model checkers have enabled the integration of formal property verification with the conventional testbench based methods in the overall verification plan. This has led to significant verification productivity across the entire design flow (from architectural verification to post-silicon debugging). As verification productivity is improved, debugging efficiency has become more important than before. In this paper, we discuss how formal technology can be leveraged to bring efficiency in the debugging process. In particular, we discuss how "behavioral indexing" enables a top-down view of the counter-example and facilitates debugging by overlaying a higher abstraction view on the bit-level counter-example. We also discuss how formal technology can be leveraged to do "what-if" analysis to localize the root cause of the bug. We also discuss how formal technology supports the even more challenging task of traceless debugging (the process of debugging the "absence of witness/counter-example").
Verifying large industrial designs is getting harder each day. The current verification methodologies are not able to guarantee bug free designs. Some recurrent questions during a design verification are: Which modules are most likely to contain undetected bugs? In which modules the verification team should concentrate their effort? This information is very useful, because it is better to start verifying the most bug-prone modules. In this work we present a novel approach to answer these questions. In order to identify these bug-prone modules, the revision history of the design is used. Using information of an academic experiment, we demonstrate that there is a close relationship between bugs/changes history and future bugs. Our results show that allocating modules for verification based on bugs/changes leaded to the coverage of 91.67% of future bugs, while random based strategy covered only 37.5% of the future bugs.