  Accurate delay models are important for static and dynamic timing analysis of
digital circuits, and mandatory for formal verification. However, F\"ugger et
al. [IEEE TC 2016] proved that pure and inertial delays, which are employed for
dynamic timing analysis in state-of-the-art tools like ModelSim, NC-Sim and
VCS, do not yield faithful digital circuit models. Involution delays, which are
based on delay functions that are mathematical involutions depending on the
previous-output-to-input time offset, were introduced by F\"ugger et al.
[DATE'15] as a faithful alternative (that can easily be used with existing
tools). Although involution delays were shown to predict real signal traces
reasonably accurately, any model with a deterministic delay function is
naturally limited in its modeling power. In this paper, we thus extend the
involution model, by adding non-deterministic delay variations (random or even
adversarial), and prove analytically that faithfulness is not impaired by this
generalization. Albeit the amount of non-determinism must be considerably
restricted to ensure this property, the result is surprising: the involution
model differs from non-faithful models mainly in handling fast glitch trains,
where small delay shifts have large effects. This originally suggested that
adding even small variations should break the faithfulness of the model, which
turned out not to be the case. Moreover, the results of our simulations also
confirm that this generalized involution model has larger modeling power and,
hence, applicability.
