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).
