发表机构
College of Integrated Circuits; Micro-Nano Electronics Fudan University, Shanghai, China（; ）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对离散可调时钟树中调度与实现不匹配问题，提出精确可实现性割与算术证书反馈接口，实验证明可减少oracle调用，但非通用加速方案。
AI 中文摘要
有用偏斜（useful-skew）调度可以满足时序约束，但可能无法由具有离散调优选项的固定时钟树实现。我们将这种不匹配表述为有限相对延迟集合中的精确成员资格问题，并开发了调度器与时钟树模型之间可检查的反馈接口。算术证书（arithmetic certificates）解释不可实现的目标，而树特定收缩（tree-specific contraction）减少了投影到选定汇点（sinks）上的精确关系的结构规模。这些关系成为可实现性割（realizability cuts），与相同证书支撑（certificate support）上的 no-good 割相比，可以排除更多候选，包括线性不等式无法分离的离散空洞（discrete holes）。受控实验确认了更少的 oracle 调用和更快的投影构建。它们也揭示了重要限制：全局最小证书可能得不偿失，紧凑的算术反馈可能无法处理非奇偶障碍（non-parity obstructions），并且在测试的加法模型上，直接的整体优化仍然更快。其贡献是一个精确的、可独立验证的调度器-树接口，而非声称通用求解器加速或物理签核（physical signoff）。
英文摘要
Useful-skew schedules can satisfy timing constraints yet remain unrealizable by a fixed clock tree with discrete tuning choices. We formulate this mismatch as exact membership in a finite relative-latency set and develop a checkable feedback interface between the scheduler and the tree model. Arithmetic certificates explain unrealizable targets, while tree-specific contraction reduces the structural size of the exact relations projected onto selected sinks. These relations become realizability cuts that can exclude more candidates than a no-good on the same certificate support, including discrete holes that linear inequalities cannot separate. Controlled experiments confirm fewer oracle calls and faster projection construction. They also expose important limits: globally minimum certificates can cost more than they save, compact arithmetic feedback can fail on non-parity obstructions, and direct monolithic optimization remains faster on the tested additive models. The contribution is an exact, independently verifiable scheduler--tree interface, rather than a claim of universal solver acceleration or physical signoff.
