binary-decision-diagram - BDD/CuDD可以用来描述时序逻辑吗

Question

我知道用 BDD/CuDD 描述组合电路很常见。但是是否可以将 BDD 用于 DFF/Latch 等时序逻辑电路？似乎不可能？或者可能只是忽略 CK/D 时序要求并将它们视为简单逻辑？我相信合成算法使用了一些技术来处理

有什么相关的论文/书吗？来自伯克利的 ABC 包裹会这样做吗？