Patent ID: 8473895

Claim:
A computer-implemented method for exploring a design space, the method comprising: receiving a design specification expressed in a modeling language, the design specification describing a collection of constraints that acceptable architectures are expected to satisfy; symbolically executing the design specification to provide a logical formula, wherein said symbolically executing comprises executing the design specification over a set of symbolic inputs to produce the logical formula and wherein the logical formula is quantifier-free; in an instance when at least two solutions to the logical formula exist, interacting with a theorem prover module to identify a first solution to the logical formula and a second solution to the logical formula within the design space, wherein: the first solution pertains to a first architecture that satisfies the constraints, and the second solution pertains to a second architecture that also satisfies the constraints and is different than the first architecture; and converting the first solution and the second solution into a user-interpretable form, wherein at least the interacting with the theorem prover module is performed by a processing device.