Symbolic Timing Analysis of Digital Circuits Using Analytic Delay Functions

TL;DR

This work tackles the challenge of timing verification without expensive SPICE simulations by leveraging analytic delay functions $\delta(T,\Delta)$ for 2-input NOR/NAND/Muller-C gates. It presents a symbolic framework that, for a fixed input-transition order, composes these delay expressions to produce closed-form symbolic output-transition times dependent on symbolic inputs and gate parameters. The approach supports sensitivity analysis and compatibility with formal verification workflows by embedding symbolic constraints into SAT/SMT proofs, demonstrated through a SageMath prototype applied to the NOR-based c17 slack benchmark. The results show successful propagation of symbolic delays across multiple gate layers and capture both drafting and MIS effects without analog traces, highlighting potential for path validation, parameter sweeps, and eventual order exploration via symbolic execution. This work thus offers a pathway toward faster, parameter-aware, circuit-level timing analysis and verification without full SPICE-based simulations.

Abstract

We propose a novel approach to symbolic timing analysis for digital integrated circuits based on recently developed analytic delay formulas for 2-input NOR, NAND, and Muller-C gates by Ferdowsi et al. (NAHS 2025). Given a fixed order of the transitions of all input and internal signals of a circuit, our framework computes closed-form analytic delay expressions for all the internal signal transition times that depend on (i) the symbolic transition times of the relevant input signals and (ii) the model parameters of the relevant gates. The resulting formulas facilitate per-transition timing analysis without any simulation, by instantiating the symbolic input transition times and the gate parameters. More importantly, however, they also enable an \emph{analytic} study of the dependencies of certain timing properties on input signals and gate parameters. For instance, differentiating a symbolic delay expression with respect to a gate parameter or input transition time enables sensitivity analysis. As a proof of concept, we implement our approach using the computer algebra system SageMath and apply it to the NOR-gate version of the c17 slack benchmark circuit.

Figures (2)

• Figure 1: C17 with NOR gates.
• Figure 2: Timing diagram showing the first formula $t_{o1}$ symbolically.