Verification of Modulo Counter Circuits
摘要
In this section, the verification of modulo counters it viewed. The introduced model checking variant is further extended to be applicable to non-bijective functions. This is analyzed with respect to the required resources.