Abstraction techniques to improve scalability of equivalence verification for NCL circuits

Asynchronous NULL convention logic (NCL) circuits are dual‐rail quasi‐delay‐insensitive circuits that have many applications in high radiation and extreme temperature fluctuation environments such as space exploration. Two abstraction techniques are proposed that can be used to drastically improve the efficiency and scalability of formal equivalence verification targeted at NCL circuits. The effectiveness of the abstraction techniques have been demonstrated using a number of multiply and accumulate circuit benchmarks.