We propose quantum circuit verification approaches, containing partial equivalence checking and a vanishing-state-based assertion framework. The former extends equivalence definitions to improve synthesis and simplification flexibility; the latter automatically generates assertion circuits to monitor states during execution and detect errors early, enhancing reliability and operational efficiency.

We introduce the first verification method for observational equivalence in quantum circuits. Using decision diagrams, nonlinear measurements are reduced from exponential complexity to linear times of Boolean operations. Our dynamic assertion framework monitors quantum states without altering them, which is general and can automatically generate implementable circuits.

We propose partial equivalence, relaxing quantum circuit equivalence and enhancing synthesis flexibility. From definitions to algorithms, our framework fills development gaps. The dynamic assertion framework is the first and only method to systematically and automatically generate quantum assertion circuits, playing a key role in reducing costs and improving efficiency in quantum computation.