Author

Min Li

View on Semantic Scholar

2 papers indexed here

We haven’t gathered this author’s papers yet. Follow them and we’ll fetch their work.

Not the right person? Other researchers publish under this name.

Review Aug 2026

Spec-Driven Hardware Evolution via Executable Contract Refinement and Proof-Guided RTL Update

Hardware development is inherently evolutionary: major revisions typically begin by changing intended behavior and then updating a previously validated implementation, rather than regenerating RTL from scratch. Yet most recent LLM-based hardware research still frames the task primarily as prompt-to-RTL generation, offering limited support for semantic version evolution of trusted legacy designs. We present spec-driven hardware evolution, a contract-centered formulation for RTL version iteration. Instead of treating a new feature request as a direct prompt for RTL generation, we refine it into a reviewed executable contract for the next version. This contract specifies what must hold at the externally visible transactional level through a behavior-level reference together with explicit observation and checking semantics, while leaving how the change is realized in RTL to the evolution process. Based on this formulation, we organize hardware evolution into four stages: Specify, Plan, Implement, and Validate. After contract approval, the remaining stages proceed automatically: Plan derives cross-version semantic deltas and localizes affected RTL regions, aided by mutation-based semantic probing; Implement and Validate then perform legacy-aware RTL update under proof-guided checking and iterative repair. We evaluate the framework on a controlled version-evolution case study of a representative TPU datapath block under data-format changes. The results support the feasibility of contract-driven hardware evolution and demonstrate that the proposed backend workflow can effectively drive validated legacy RTL toward next-version functional convergence under a reviewed executable contract. An anonymous artifact for reproducibility is available at https://anonymous.4open.science/r/SDHE-3A6C.

Shibo Zhao, Yang Zhang, M. Tao et al. · 0 citations

Preprint Jul 2026

Arisca: A Parameterized Symbolic Algebra Framework for Arithmetic Circuit Verification

Formal verification of highly optimized arithmetic circuits at the gate-level remains a significant challenge due to the state space explosion problem. Although Symbolic Computer Algebra (SCA) offers a scalable theoretical foundation by modeling circuits as multivariate polynomials, practical implementations frequently suffer from the explosion of the size of intermediate polynomials. State-of-the-art SCA tools typically rely on fixed heuristics and restrict their application to standard multipliers. A fixed heuristic is insufficient for structurally diverse arithmetic circuits, as it often fails to generalize across all cases. In this paper, we introduce Arisca, an open-source parameterized verification framework for \textbf{Ari}thmetic circuits using \textbf{S}ymbolic \textbf{C}omputer \textbf{A}lgebra. Arisca establishes a generalized parameter space that unifies previously isolated state-of-the-art (SOTA) techniques as specific configurations within a broader algebraic reduction theory. To fundamentally transplant and elevate previous methods, we propose several algorithmic improvements, such as an HA-preserving extraction strategy, density-based vanishing detection, and conservative polynomial size estimation. In addition, Arisca expands the verification scope to encompass general arithmetic circuits with any combination of addition and multiplication, such as multiply-accumulators and dot-product units. Extensive evaluations demonstrate that Arisca achieves SOTA performance in a comprehensive suite of multiplier benchmarks and a diverse array of practical arithmetic cases.

Kezhi Li, Min Li, Qiang Xu · 0 citations