Method and system for automated design and design-space exploration

A non-transitory computer-readable storage medium storing instructions that when executed by a computer cause the computer to perform a method for automated design of a physical computational system, the method comprising:

• obtaining a component library comprising a plurality of computational components;
• receiving design requirements of the physical computational system;
• building a plurality of universal component cells, wherein a respective universal component cell is configurable, by a selection signal, to behave as one of the plurality of computational components;
• constructing a candidate computational system using the plurality of universal component cells;
• encoding the received design requirements and the candidate computational system into a single logic formula by constructing a miter structure based on the design requirements and the candidate computational system, wherein variables within the single logic formula comprise at least inputs, outputs, and selection signals of the universal component cells within the candidate computational system, wherein the single logic formula comprises a quantified Boolean formula (QBF);
• executing, by a computer, a QBF solver to solve the QBF in order to obtain at least one design solution for the physical computational system, wherein solving the QBF comprises searching for satisfying assignments to the selection signals;
• and
• outputting the at least one design solution, thereby facilitating a system builder to build the physical computational system.

A computer system for automated design of a physical computational system, the system comprising:

• a processor;
• and
• a storage device coupled to the processor and storing instructions, which when executed by the processor cause the processor to perform a method, wherein the method comprises:
• obtaining a component library comprising a plurality of computational components;
• receiving design requirements of the physical computational system;
• building a plurality of universal component cells, wherein a respective universal component cell is configurable, by a selection signal, to behave as one of the plurality of computational components;
• constructing a candidate computational system using the plurality of universal component cells;
• encoding the received design requirements and the candidate computational system into a single logic formula by constructing a miter structure based on the design requirements and the candidate computational system, wherein variables within the single logic formula comprise at least inputs, outputs, and selection signals of the universal component cells within the candidate computational system, wherein the single logic formula comprises a quantified Boolean formula (QBF);
• executing, by the computer system, a QBF solver to solve the QBF in order to obtain at least one design solution for the physical computational system, wherein solving the QBF comprises searching for satisfying assignments to the selection signals;
• and
• outputting the at least one design solution, thereby facilitating a system builder to build the physical computational system.