paper-with-me

Papers

Analogous Alignments: Digital "Formally" meets Analog

2024-09-23 · Hansa Mohanty, Deepak Narayan Gadde

The complexity of modern-day System-on-Chips (SoCs) is continually increasing, and it becomes increasingly challenging to deliver dependable and credible chips in a short time-to-market. Especially, in the case of test chips, where the aim is to study the feasibility of the design, time is a crucial factor. Pre-silicon functional verification is one of the main contributors that makes up a large portion of the product development cycle. Verification engineers often loosely verify test chips that turn out to be non-functional on the silicon, ultimately resulting in expensive re-spins. To left-shift the verification efforts, formal verification is a powerful methodology that aims to exhaustively verify designs, giving better confidence in the overall quality. This paper focuses on the pragmatic formal verification of a mixed signal Intellectual Property (IP) that has a combination of digital and analog blocks. This paper discusses a novel approach of including the analog behavioral model into the formal verification setup. Digital and Analog Mixed-Signal (AMS) designs, which are fundamentally different in nature, are integrated seamlessly in a formal verification setup, a concept that can be referred to as "Analogous Alignments". Our formal setup leverages powerful formal techniques such as FPV, CSR verification, and connectivity checks. The properties used for FPV are auto-generated using a metamodeling framework. The paper also discusses the challenges faced especially related to state-space explosion, non-compatibility of formal with AMS models, and techniques to mitigate them such as k-induction. With this verification approach, we were able to exhaustively verify the design within a reasonable time and with sufficient coverage. We also reported several bugs at an early stage, making the complete design verification process iterative and effective.

📄 PDF Abstract BibTeX arXiv:2409.15013

Code (0)

등록된 구현이 없습니다.

Similar Papers 제목 키워드 기반

BLANT: Basic Local Alignment of Network Topology, Part 1: Seeding local alignments with unambiguous 8-node graphlets

2022-07-10 · Patrick Wang, Henry Ye, Wayne B Hayes

BLAST is a standard tool in bioinformatics for creating local sequence alignments using a "seed-and-extend" approach. Here we introduce an analogous seed-and-extend algorithm that produces local network alignments: BLANT…

Specificity

Scales and Hedges in a Logic with Analogous Semantics

2022-01-21 · Hedda R. Schmidtke, Sara Coelho

Logics with analogous semantics, such as Fuzzy Logic, have a number of explanatory and application advantages, the most well-known being the ability to help experts develop control systems. From a cognitive systems persp…

Decision MakingLogical Reasoning

Past Meets Present: Creating Historical Analogy with Large Language Models

2024-09-23 · Nianqi Li, Siyu Yuan, Jiangjie Chen, Jiaqing Liang 외

Historical analogies, which compare known past events with contemporary but unfamiliar events, are important abilities that help people make decisions and understand the world. However, research in applied history sugges…

Retrieval

Waves and symbols in neuromorphic hardware: from analog signal processing to digital computing on the same computational substrate

2025-02-27 · Dmitrii Zendrikov, Alessio Franci, Giacomo Indiveri

Neural systems use the same underlying computational substrate to carry out analog filtering and signal processing operations, as well as discrete symbol manipulation and digital computation. Inspired by the computationa…

Training of mixed-signal optical convolutional neural network with reduced quantization level

2020-08-20 · Joseph Ulseth, Zheyuan Zhu, Guifang Li, Shuo Pang

Mixed-signal artificial neural networks (ANNs) that employ analog matrix-multiplication accelerators can achieve higher speed and improved power efficiency. Though analog computing is known to be susceptible to noise and…

Quantization