Methods and apparatus for Boolean equivalency checking in the presence of voting logic

An apparatus for designing a circuit, comprising:

• a computer having:
• a memory;
• improved Boolean equivalency checking (BEC) code stored in the memory;
• and
• a processor coupled to the memory and adapted to execute the improved BEC code;
• wherein the improved BEC code is adapted to:
• receive a model of an original circuit design including a latch;
• receive a model of a modified version of the original circuit design, wherein the modified version of the original circuit design includes a set of latches associated with the latch of the original circuit design and voting logic having inputs coupled to respective outputs of latches in the latch set and having outputs coupled to combinational logic;
• the set of latches including N latches, where N is an odd number;
• determine subsets of the set of latches, wherein each subset is a unique group of M latches and where M is the integer value of N/2;
• during Boolean equivalency checking (BEC), inject an error on at most a largest minority of the respective inputs of the voting logic to test the voting logic function, for each of the subsets, injecting an error on each latch in the subset;
• and
• for each of the subsets, after injecting an error on each latch in the subset, testing the voting logic by determining a logical function at a point of the modified version of the original circuit that is downstream from the voting logic, wherein such logical function is based on the output of the voting logic.