Ordering-Relation Abstraction for Formal Verification of Bubble Errors\\ in CARRY8-Based Tapped Delay Lines

Reproducibility artifact for the FMCAD 2026 paper "Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines". Contains NuSMV/nuXmv models, automated verification scripts, and pre-computed logs that reproduce all results from the paper (Tables 1–6, Theorems T1–T5). Contents: Hand-written N=8 reference NuSMV model (638 lines, 55 CTL/LTL specs)Parameterised Python generator for arbitrary tap counts (N ≥ 2)Auto-generated models for N ∈ {8, 16, 40, 80, 160}Dual-engine (BDD + IC3) scaling driverOne-command reproduction script with pass/fail checksPre-computed verification logs for all experimentsRequirements: Python 3.8+ (standard library only), NuSMV 2.7.1 and/or nuXmv 2.1.0 (free downloads, no compilation needed).本工件为FMCAD 2026会议论文《基于CARRY8的抽头延迟线气泡错误形式验证的序关系抽象》（"Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines"）的可复现研究工件。 本工件包含NuSMV/nuXmv模型、自动化验证脚本以及预计算验证日志，可复现论文中的全部实验结果（表1至表6、定理T1至T5）。 内容详情： 1. 手写的N=8基准NuSMV模型（共638行，包含55个计算树逻辑（CTL）、线性时序逻辑（LTL）规范） 2. 支持任意抽头数（N≥2）的参数化Python生成器 3. 针对N取值为{8、16、40、80、160}的自动生成模型 4. 双引擎（二元决策图（BDD）+ IC3）规模扩展验证驱动程序 5. 单命令复现脚本，附带通过/失败校验机制 6. 所有实验的预计算验证日志 运行要求：Python 3.8及以上版本（仅依赖Python标准库）、NuSMV 2.7.1及/或nuXmv 2.1.0（可免费下载，无需编译）。