1. A method to check correspondence between different representations of a circuit, comprising: abstracting a first computer language representation of the circuit to form a first abstract model of the circuit; abstracting a second computer language representation of the circuit to form a second abstract model of the circuit; forming a product machine using the first and second abstract models; and checking correspondence between the first and second abstract models using the product machine.