arXiv subjects

Matthias Jung

Publications and source records attributed to Matthias Jung.

13 recordsLinked to original sources

arXiv2026

Autoformalizing Memory Specifications with Agents

The primary goal of Design Verification (DV) is to ensure that a proposed chip design implementation (either in code, or physical form) exactly matches its specification and is free of functional errors in order to avoid costly re-designs. Achieving this often demands extensive manual interpretation, translating the specification document into a formal, testable representation. While AI has made progress in DV, current approaches typically focus on narrow, isolated tasks rather than full end-to-end specification compliance of modern chip designs, failing to capture the complexity of real-world verification. Our method automatically formalizes natural language memory chip specifications, for industry relevant Dynamic Random Access Memory (DRAM) standards, into a formal representation called DRAMPyML that can be used for downstream DV tasks like the generation of SystemVerilog assertions, stimulus, and functional coverage. We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities (and new approaches) at hardware autoformalization.

cs.AR↗

arXiv2026

DRAMPyML: A Formal Description of DRAM Protocols with Timed Petri Nets

The JEDEC committee defines various domain-specific DRAM standards. These standards feature increasingly complex and evolving protocol specifications, which are detailed in timing diagrams and command tables. Understanding these protocols is becoming progressively challenging as new features and complex device hierarchies are difficult to comprehend without an expressive model. While each JEDEC standard features a simplified state machine, this state machine fails to reflect the parallel operation of memory banks. In this paper, we present an evolved modeling approach based on timed Petri nets and Python. This model provides a more accurate representation of DRAM protocols, making them easier to understand and directly executable, which enables the evaluation of interesting metrics and the verification of controller RTL models, DRAM logic and memory simulators.

cs.AR↗

arXiv2025

Architecture, Simulation and Software Stack to Support Post-CMOS Accelerators: The ARCHYTAS Project

ARCHYTAS aims to design and evaluate non-conventional hardware accelerators, in particular, optoelectronic, volatile and non-volatile processing-in-memory, and neuromorphic, to tackle the power, efficiency, and scalability bottlenecks of AI with an emphasis on defense use cases (e.g., autonomous vehicles, surveillance drones, maritime and space platforms). In this paper, we present the system architecture and software stack that ARCHYTAS will develop to integrate and support those accelerators, as well as the simulation software needed for early prototyping of the full system and its components.

cs.AR↗

arXiv2025

RoentMod: A Synthetic Chest X-Ray Modification Model to Identify and Correct Image Interpretation Model Shortcuts

Chest radiographs (CXRs) are among the most common tests in medicine. Automated image interpretation may reduce radiologists\' workload and expand access to diagnostic expertise. Deep learning multi-task and foundation models have shown strong performance for CXR interpretation but are vulnerable to shortcut learning, where models rely on spurious and off-target correlations rather than clinically relevant features to make decisions. We introduce RoentMod, a counterfactual image editing framework that generates anatomically realistic CXRs with user-specified, synthetic pathology while preserving unrelated anatomical features of the original scan. RoentMod combines an open-source medical image generator (RoentGen) with an image-to-image modification model without requiring retraining. In reader studies with board-certified radiologists and radiology residents, RoentMod-produced images appeared realistic in 93\% of cases, correctly incorporated the specified finding in 89-99\% of cases, and preserved native anatomy comparable to real follow-up CXRs. Using RoentMod, we demonstrate that state-of-the-art multi-task and foundation models frequently exploit off-target pathology as shortcuts, limiting their specificity. Incorporating RoentMod-generated counterfactual images during training mitigated this vulnerability, improving model discrimination across multiple pathologies by 3-19\% AUC in internal validation and by 1-11\% for 5 out of 6 tested pathologies in external testing. These findings establish RoentMod as a broadly applicable tool for probing and correcting shortcut learning in medical AI. By enabling controlled counterfactual interventions, RoentMod enhances the robustness and interpretability of CXR interpretation models and provides a generalizable strategy for improving foundation models in medical imaging.

eess.IV↗

arXiv2024

VIBESegmentator: Full Body MRI Segmentation for the NAKO and UK Biobank

Objectives: To present a publicly available deep learning-based torso segmentation model that provides comprehensive voxel-wise coverage, including delineations that extend to the boundaries of anatomical compartments. Materials and Methods: We extracted preliminary segmentations from TotalSegmentator, spine, and body composition models for Magnetic Resonance Tomography (MR) images, then improved them iteratively and retrained an nnUNet model. Using a random retrospective subset of German National Cohort (NAKO), UK Biobank, internal MR and Computed Tomography (CT) data (Training: 2897 series from 626 subjects, 290 female; mean age 53+-16; 3-fold-cross validation (20% hold-out). Internal testing 36 series from 12 subjects, 6 male; mean age 60+-11), we segmented 71 structures in torso MR and 72 in CT images: 20 organs, 10 muscles, 19 vessels, 16 bones, ribs in CT, intervertebral discs, spinal cord, spinal canal and body composition (subcutaneous fat, unclassified muscles and visceral fat). For external validation, we used existing automatic organ segmentations, independent ground truth segmentations on gradient echo images, and the Amos data. We used non-parametric bootstrapping for confidence intervals and Wilcoxon rank-sum test for computing statistical significance. Results: We achieved an average Dice score of 0.90+-0.06 on our internal gradient echo test set, which included 71 semantic segmentation labels. Our model ties with the best model on Amos with a Dice of 0,81+-0.14, while having a larger field of view and a considerably higher number structures included. Conclusion: Our work presents a publicly available full-torso segmentation model for MRI and CT images that classifies almost all subject voxels to date.

eess.IV↗

arXiv2024

TotalSegmentator MRI: Robust Sequence-independent Segmentation of Multiple Anatomic Structures in MRI

Since the introduction of TotalSegmentator CT, there is demand for a similar robust automated MRI segmentation tool that can be applied across all MRI sequences and anatomic structures. In this retrospective study, a nnU-Net model (TotalSegmentator) was trained on MRI and CT examinations to segment 80 anatomic structures relevant for use cases such as organ volumetry, disease characterization, surgical planning and opportunistic screening. Examinations were randomly sampled from routine clinical studies to represent real-world examples. Dice scores were calculated between the predicted segmentations and expert radiologist reference standard segmentations to evaluate model performance on an internal test set, two external test sets and against two publicly available models, and TotalSegmentator CT. The model was applied to an internal dataset containing abdominal MRIs to investigate age-dependent volume changes. A total of 1143 examinations (616 MRIs, 527 CTs) (median age 61 years, IQR 50-72) were split into training (n=1088, CT and MRI) and an internal test set (n=55; only MRI), two external test sets (AMOS, n=20; CHAOS, n=20; only MRI), and an internal aging-study dataset of 8672 abdominal MRIs (median age 59 years, IQR 45-70) were included. The model showed a Dice Score of 0.839 on the internal test set and outperformed two other models (Dice Score, 0.862 versus 0.759; and 0.838 versus 0.560; p<.001 for both). The proposed open-source, easy-to-use model allows for automatic, robust segmentation of 80 structures, extending the capabilities of TotalSegmentator to MRIs of any sequence. The ready-to-use online tool is available at https://totalsegmentator.com, the model at https://github.com/wasserth/TotalSegmentator, and the dataset at https://zenodo.org/records/14710732.

eess.IV↗

arXiv2024

QCEDA: Using Quantum Computers for EDA

The field of Electronic Design Automation (EDA) is crucial for microelectronics, but the increasing complexity of Integrated Circuits (ICs) poses challenges for conventional EDA: Corresponding problems are often NP-hard and are therefore in general solved by heuristics, not guaranteeing optimal solutions. Quantum computers may offer better solutions due to their potential for optimization through entanglement, superposition, and interference. Most of the works in the area of EDA and quantum computers focus on how to use EDA for building quantum circuits. However, almost no research focuses on exploiting quantum computers for solving EDA problems. Therefore, this paper investigates the feasibility and potential of quantum computing for a typical EDA optimization problem broken down to the Min-$k$-Union problem. The problem is mathematically transformed into a Quadratic Unconstrained Binary Optimization (QUBO) problem, which was successfully solved on an IBM quantum computer and a D-Wave quantum annealer.

quant-ph↗

arXiv2022

A Framework for Formal Verification of DRAM Controllers

The large number of recent JEDEC DRAM standard releases and their increasing feature set makes it difficult for designers to rapidly upgrade the memory controller IPs to each new standard. Especially the hardware verification is challenging due to the higher protocol complexity of standards like DDR5, LPDDR5 or HBM3 in comparison with their predecessors. With traditional simulation-based verification it is laborious to guarantee the coverage of all possible states, especially for control flow rich memory controllers. This has a direct impact on the time-to-market. A promising alternative is formal verification because it allows to ensure protocol compliance based on mathematical proofs. However, with regard to memory controllers no fully-automated verification process has been presented in the state-of-the-art yet, which means there is still a potential risk of human error. In this paper we present a framework that automatically generates SystemVerilog Assertions for a DRAM protocol. In addition, we show how the framework can be used efficiently for different tasks of memory controller development.

cs.FL↗

arXiv2022

Unveiling the Real Performance of LPDDR5 Memories

LPDDR5 is the latest low-power DRAM standard and expected to be used in various application fields. The vendors have published promising peak bandwidths up to 50 % higher than those of the predecessor LPDDR4. In this paper we evaluate the best-case and worst-case real bandwidth utilization of different LPDDR5 configurations and compare the results to corresponding LPDDR4 configurations. We also show that an upgrade from LPDDR4 to LPDDR5 does not always bring a bandwidth advantage and that some LPDDR5 configurations should be avoided for specific workloads.

cs.AR↗

arXiv2020

The gem5 Simulator: Version 20.0+

The open-source and community-supported gem5 simulator is one of the most popular tools for computer architecture research. This simulation infrastructure allows researchers to model modern computer hardware at the cycle level, and it has enough fidelity to boot unmodified Linux-based operating systems and run full applications for multiple architectures including x86, Arm, and RISC-V. The gem5 simulator has been under active development over the last nine years since the original gem5 release. In this time, there have been over 7500 commits to the codebase from over 250 unique contributors which have improved the simulator by adding new features, fixing bugs, and increasing the code quality. In this paper, we give and overview of gem5's usage and features, describe the current state of the gem5 simulator, and enumerate the major changes since the initial release of gem5. We also discuss how the gem5 simulator has transitioned to a formal governance model to enable continued improvement and community support for the next 20 years of computer architecture research.

cs.AR↗

arXiv2019

eBrainII: A 3 kW Realtime Custom 3D DRAM integrated ASIC implementation of a Biologically Plausible Model of a Human Scale Cortex

The Artificial Neural Networks (ANNs) like CNN/DNN and LSTM are not biologically plausible and in spite of their initial success, they cannot attain the cognitive capabilities enabled by the dynamic hierarchical associative memory systems of biological brains. The biologically plausible spiking brain models, for e.g. cortex, basal ganglia and amygdala have a greater potential to achieve biological brain like cognitive capabilities. Bayesian Confidence Propagation Neural Network (BCPNN) is a biologically plausible spiking model of cortex. A human scale model of BCPNN in real time requires 162 TFlops/s, 50 TBs of synaptic weight storage to be accessed with a bandwidth of 200 TBs. The spiking bandwidth is relatively modest at 250 GBs/s. A hand optimized implementation of rodent scale BCPNN has been implemented on Tesla K80 GPUs require 3 kW, we extrapolate from that a human scale network will require 3 MW. These power numbers rule out such implementations for field deployment as advanced cognition engines in embedded systems. The key innovation that this paper reports is that it is feasible and affordable to implement real time BCPNN as a custom tiled ASIC in 28 nm technology with custom 3D DRAM - eBrain II - that consumes 3 kWs for human scale and 12 W for rodent scale cortex model. Such implementations eminently fulfill the demands for field deployment.

cs.DC↗

arXiv2018

Deep-CLASS at ISIC Machine Learning Challenge 2018

This paper reports the method and evaluation results of MedAusbild team for ISIC challenge task. Since early 2017, our team has worked on melanoma classification [1][6], and has employed deep learning since beginning of 2018 [7]. Deep learning helps researchers absolutely to treat and detect diseases by analyzing medical data (e.g., medical images). One of the representative models among the various deep-learning models is a convolutional neural network (CNN). Although our team has an experience with segmentation and classification of benign and malignant skin-lesions, we have participated in the task 3 of ISIC Challenge 2018 for classification of seven skin diseases, explained in this paper.

cs.LG↗

arXiv2018

Integrating DRAM Power-Down Modes in gem5 and Quantifying their Impact

Across applications, DRAM is a significant contributor to the overall system power, with the DRAM access energy per bit up to three orders of magnitude higher compared to on-chip memory accesses. To improve the power efficiency, DRAM technology incorporates multiple power-down modes, each with different trade-offs between achievable power savings and performance impact due to entry and exit delay requirements. Accurate modeling of these low power modes and entry and exit control is crucial to analyze the trade-offs across controller configurations and workloads with varied memory access characteristics. To address this, we integrate the power-down modes into the DRAM controller model in the open-source simulator gem5. This is the first publicly available full-system simulator with DRAM power-down modes, providing the research community a tool for DRAM power analysis for a breadth of use cases. We validate the power-down functionality with sweep tests, which trigger defined memory access characteristics. We further evaluate the model with real HPC workloads, illustrating the value of integrating low power functionality into a full system simulator.

cs.AR↗