In automating the verification of analog/mixed-signal (AMS) circuits, it essential to have a specification language that can describe the behavior that needs to be checked. Although powerful and very expressive, many such languages have a steep …
The enormous number of states reachable during explicit model checking is the main bottleneck for scalability. This paper presents approaches of using decision diagrams to represent very large state space compactly and efficiently. This is possible …
Efficacy of partial order reduction in reducing state space relies on adequate extraction of the independence relation among possible behaviors. However, traditional approaches by statically analyzing system model structures are often not able to …