IP Library › Granted Patent US 12,437,133
Granted Patent B2
US 12,437,133 · App. 17/695,387 · Granted Oct 7, 2025

Property-driven automatic generation of reduced component hardware

Inventors: Rakesh Kumar (Urbana, IL); Nathaniel Lewis Bleier (Urbana, IL)
Assignee: The Board of Trustees of the University of Illinois
G06F30/327G06F9/3016G06F9/3836G06F30/3323G06F30/337G06F2119/16H03K19/096
View Patent ↗
Loading inventors, assignments & file history…
Monitor This Case
Get email alerts when status or documents change.
Order Certified Copies
Most orders are placed with the USPTO same day — all within 24 business hours.
Order via The Patent Place →
Pre-filled with this patent's details
Quick Facts
Patent No.
US 12,437,133
App. No.
17/695,387
Granted
Oct 7, 2025
Kind
B2
Abstract

An embodiment may involve obtaining a specification of connectivity between a plurality of electronic components, a property library of logical validations, and a set of restrictions for an execution environment of the electronic components, wherein each of the electronic components is associated with at least one of the logical validations; determining that, according to properties in the property library applied to their associated electronic components, a subset of the electronic components exhibit invariance within the execution environment; based on the subset of the electronic components that exhibit invariance within the execution environment, rewiring the connectivity between the plurality of electronic components; and performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment.

Claims (43)

1. A computer-implemented method comprising:

obtaining a specification of connectivity between a plurality of electronic components, a property library of logical validations, and a set of restrictions for an execution environment of the electronic components, wherein each of the electronic components is associated with at least one of the logical validations;

determining that, according to properties in the property library applied to their associated electronic components, a subset of the electronic components exhibit invariance within the execution environment;

based on the subset of the electronic components that exhibit invariance within the execution environment, rewiring the connectivity between the plurality of electronic components; and

performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment.

2. The computer-implemented method of claim 1 , wherein the properties in the property library include logic statements specifying invariance within inputs of an electronic component, outputs of the electronic component, or both the inputs and the outputs of the electronic component.

3. The computer-implemented method of claim 1 , wherein the execution environment includes a workload executable by the plurality of electronic components.

4. The computer-implemented method of claim 1 , wherein simplifying at least some of the subset of the electronic components that exhibit invariance within the execution environment comprises:

reducing a transistor count of the subset of the electronic components that exhibit invariance within the execution environment.

5. The computer-implemented method of claim 1 , wherein simplifying at least some of the subset of the electronic components that exhibit invariance within the execution environment comprises:

removing at least some of the subset of the electronic components that exhibit invariance within the execution environment.

6. The computer-implemented method of claim 1 , wherein performing logic synthesis on the connectivity between the plurality of electronic components as rewired results in a simplified plurality of electronic components that is functionality equivalent to the plurality of electronic components when used within the execution environment.

7. The computer-implemented method of claim 1 , wherein each of the electronic components is a logic gate of a synchronous digital circuit.

8. The computer-implemented method of claim 7 , wherein the synchronous digital circuit has an obfuscated design.

9. The computer-implemented method of claim 1 , wherein determining that the subset of the electronic components exhibit invariance within the execution environment comprises:

determining that logic gates of the subset of the electronic components have constant output values within the execution environment.

10. The computer-implemented method of claim 9 , wherein performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment comprises:

removing at least some of the logic gates of the subset of the electronic components that have constant output values within the execution environment.

11. Computer-implemented method of claim 9 , wherein performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment comprises:

replacing at least some of the logic gates of the subset of the electronic components that have constant output values within the execution environment with simpler gates.

12. The computer-implemented method of claim 1 , wherein determining that the subset of the electronic components exhibit invariance within the execution environment comprises:

transforming the plurality of electronic components into a transition system representation;

transforming the properties in the property library and the execution environment into automata; and

applying the automata to the transition system representation.

13. The computer-implemented method of claim 1 , wherein the plurality of electronic components defines a microprocessor with an instruction set, wherein the properties encode instructions of the instruction set, wherein the execution environment defines a reduced version of the instruction set, and wherein the plurality of electronic components as rewired supports the reduced version of the instruction set.

14. The computer-implemented method of claim 13 , wherein the execution environment also defines constraints on memory input ports within the plurality of electronic components.

15. The computer-implemented method of claim 13 , wherein the execution environment also defines cutpoints within the plurality of electronic components that align the instructions of the instruction set.

16. An article of manufacture including a non-transitory computer-readable medium, having stored thereon program instructions that, when executed by a computing system, cause the computing system to perform operations comprising:

obtaining a specification of connectivity between a plurality of electronic components, a property library of logical validations, and a set of restrictions for an execution environment of the electronic components, wherein each of the electronic components is associated with at least one of the logical validations;

determining that, according to properties in the property library applied to their associated electronic components, a subset of the electronic components exhibit invariance within the execution environment;

based on the subset of the electronic components that exhibit invariance within the execution environment, rewiring the connectivity between the plurality of electronic components; and

performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment.

17. The article of manufacture of claim 16 , wherein performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment comprises:

removing at least some logic gates of the subset of the electronic components that have constant output values within the execution environment.

18. The article of manufacture of claim 16 , wherein performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment comprises:

replacing at least some logic gates of the subset of the electronic components that have constant output values within the execution environment with simpler gates.

19. The article of manufacture of claim 16 , wherein the plurality of electronic components defines a microprocessor with an instruction set, wherein the properties encode instructions of the instruction set, wherein the execution environment defines a reduced version of the instruction set, and wherein the plurality of electronic components as rewired supports the reduced version of the instruction set.

20. A method comprising:

obtaining a specification of connectivity between a plurality of electronic components, a property library of logical validations, and a set of restrictions for an execution environment of the electronic components, wherein each of the electronic components is associated with at least one of the logical validations;

determining that, according to properties in the property library applied to their associated electronic components, a subset of the electronic components exhibit invariance within the execution environment;

based on the subset of the electronic components that exhibit invariance within the execution environment, rewiring the connectivity between the plurality of electronic components;

performing logic synthesis on the connectivity between the plurality of electronic components as rewired to simplify at least some of the subset of the electronic components that exhibit invariance within the execution environment; and

fabricating a chip containing the plurality of electronic components as rewired.

Assignments (1)
ASSIGNMENT OF ASSIGNOR'S INTEREST Recorded Aug 14, 2025
From: KUMAR, RAKESH; BLEIER, NATHANIEL
To: THE BOARD OF TRUSTEES OF THE UNIVERSITY OF ILLINOIS
Reel/Frame 072019/0755 →
Continuity (2)
Provisional Application 63163335 · Mar 19, 2021
Related Publication 20220302917A1 · Sep 22, 2022
References Cited (87)
US 4960724A · Watanabe · 1990 [cited by examiner]
US 6678873B1 · Kohashi · 2004 [cited by examiner]
US 7454323B1 · Bain · 2008 [cited by examiner]
US 7757224B2 · Forin et al. · 2010 [cited by applicant]
US 9235669B2 · Prikryl et al. · 2016 [cited by applicant]
US 10671774B2 · Cherupalli et al. · 2020 [cited by applicant]
US 10866630B2 · Cherupalli et al. · 2020 [cited by applicant]
US 11210402B2 · Cherupalli et al. · 2021 [cited by applicant]
US 11210439B2 · Cherupalli et al. · 2021 [cited by applicant]
US 20070299648A1 · Levitt · 2007 [cited by examiner]
US 20190220553A1 · Renau · 2019 [cited by examiner]
US 20210041938A1 · Cherupalli et al. · 2021 [cited by applicant]
OpenCores, “Overview:: openMSP430,” Mar. 21, 2021, https://opencores.org/projects/openmsp430, printed from the World Wide Web Mar. 14, 2022. [cited by applicant]
Pan Yu, et al., “Scalable Custom Instructions Identification for Instruction-Set Extensible Processors,” In Proceedings of the 2004 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems… [cited by applicant]
Pan Yu, et al., “Characterizing Embedded Applications for Instruction-Set Extensible Processors,” In Proceedings of the 41st Annual Design Automation Conference, pp. 723-728, DAC 2004, Jun. 2004. [cited by applicant]
Dr. Dipesh Patel, “ARM Physical IP Overview,” ARM® 2012 IEEE, In 2012 IEEE International SOI Conference (SOI), pp. 1-16, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
David Patterson, et al., “The Case for the Reduced Instruction Set Computer,” ACM SIGARCH Computer Architecture News, 8(6):25-33, 1980. [cited by applicant]
Dick Price, “Pentium FDIV flaw—lessons learned,” IEEE Micro, 1995 IEEE, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
Vahid Rafe, et al., “A Survey on Coping with the State Space Explosion Problem in Model Checking,” International ResearchJournal of Applied and Basic Sciences, vol. 4 (6): 1379-1384, 2013. [cited by applicant]
Ryan Roemer, et al., “Return-Oriented Programming: Systems, Languages, and Applications, ” ACM Transactions on Information and System Security, vol. 15, No. 1, Article 2, Mar. 2012. [cited by applicant]
Douglas Almeida dos Santos, et al., “A Low-Cost Fault-Tolerant RISC-V Processor for Space Systems,” 2020 15th Design & Technology of Integrated Systems in Nanoscale Era (DTIUS), pp. 1-5, IEEE 2020. [cited by applicant]
Sergio Saponara, et al., “Application-Specific Instruction-Set Processor for Retinex-Like Image and Video Processing,” IEEE Transactions on Circuits and Systems-II: Express Briefs, vol. 54, No. 7, Jul. 2007. [cited by applicant]
Bowen Alpern, et al., “Recognizing safety and liveness*,” Distributed Computing (1987) 2:117-126. [cited by applicant]
Steve Leibson. Designing SOCs with Configured Cores: Unleashing the Tensilica Xtensa and Diamond Cores. Elsevier, 2006. [cited by applicant]
Yakun Sophia Shao, et al., “ISA-Independent Workload Characterization and its Implications for Specialized Architectures,” In 2013 IEEE International Symposium on Performance Analysis of Systems and Software (ISPASS), p… [cited by applicant]
Jeckson Dellagostin Souza, et al., “Trimming the ISA to Optimize Area and EDP Heterogeneous CMPs,” 2019 31st International Symposium on Computer Architecture and High Performance Computing (SBAC-PAD), 2019 IEEE, downloa… [cited by applicant]
Masashi Fujinami, et al., “RIDECORE: Risc-v Dynamic Exection CORE,” Mar. 28, 2016. [cited by applicant]
“The LLVM Compiler Infrastructure, LLVM Overview,” The LLVM Compiler Infrastructure Project, https://llvm.org, printed from the World Wide Web on Mar. 15, 2022. [cited by applicant]
Tong Li, et al., “Operating System Support for Overlapping-ISA Heterogeneous Multi-core Architectures, ” 2009 IEEE, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
Antti Valmari, “The State Explosion Problem,” In Advanced Course on Petri Nets, pp. 429-528. Springer, 1996. [cited by applicant]
Ashish Venkat, et al., “Harnessing ISA Diversity: Design of a Heterogeneous-ISA Chip Multiprocessor,” ACMIEEE 41st International Symposium on Computer Architecture (ISCA) 2014 IEEE, downloaded on Mar. 15, 2022 from IEEE… [cited by applicant]
Andrew Waterman, et al., “The RISC-V Instruction Set Manual, vol. I: Base User-Level ISA,” http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-62.html, May 13, 2011. [cited by applicant]
Christophe Wolinski, et al., “Automatic Selection of Application-Specific Reconfigurable Processor Extensions, ” 2008 EDAA. [cited by applicant]
Wooseok Lee, et al., “Exploring Heterogeneous-ISA Core Architectures for High-Performance and Energy-Efficient Mobile SoCs,” GLSVLSI '17, May 2017. [cited by applicant]
Bo Zhai, et al., “Energy-Efficient Subthreshold Processor Design,” IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 17, No. 8, Aug. 2009, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
Zheng Cui, et al., “Printed Electronics—Materials, Technologies and Applications,” Wiley, Higher Education Press, 2016. [cited by applicant]
ARC International, “Products & Solutions—ARChitect™ Processor Configurator—Powerfule Design Tool Automates Configurability and Extendibility of ARC Cores,” https?//web.archive.org/web/20090422141606/http://www.arc.com/c… [cited by applicant]
Christel Baier, et al., “Principles of Model Checking,” MIT Press, 2008. [cited by applicant]
David Albonesi, “The Inherent Energy Efficiency of Complexity-Adaptive Processors,” In Proc. 1998 Power-Driven Microarchitecture Workshop, pp. 107-112, 1998. [cited by applicant]
Andrei Lutas, et al., “Bitdefender—Bypassing KPTI Using the Speculative Behavior of the SWAPGS Instruction,” White Paper, 2019. [cited by applicant]
“Cortex -MO, Revision: r0p0, Technical Reference Manual,” ARM Limited, ARM DDI 0432C, 2009. [cited by applicant]
Lauranne Choquin, et al., “Arm Custom Instructions: Enabling Innovation and Greater Flexibility on Arm,” Arm, Feb. 2020. [cited by applicant]
“ARM Processor Cortex ™-MO+, Product Revision r0, Software Developers Errata Notice,” ARM, ARM-EPM-018879 v4.0, 2012. [cited by applicant]
“Arm Processor Cortex™-M4 (AT520) and Cortex-M4 with FPU (AT521), Product Revision r0, Software Developers Errata Notice,” Arm, ARM-ECM-0426805 v3, 2019. [cited by applicant]
Jonathan Bachrach, et al., “Chisel: Constructing Hardware in a Scala Embedded Language,” DAC (Design Automation Conference) 2012, pp. 1212-1221, downloaded Mar. 14, 2022 from IEEE Xplore. [cited by applicant]
Iain Bate, et al., “Use of Modern Processors in Safety-Critical Applications,” The Computer Journal, vol. 44, No. 6, pp. 531-543, Apr. 2001. [cited by applicant]
Nathaniel Bleier, et al., “Printed Microprocessors,” 2020 ACE/IEEE 47th Annual International Symposium on Computer Architecture (ISCA), pp. 213-226, IEEE 2006, downloaded on Mar. 14, 2022 from IEEE Xplore. [cited by applicant]
Edson Borin, et al., “Clustering-Based Microcode Compression,” 2006 International Conference on Computer Design, pp. 189-196, 2006 IEEE, downloaded on Mar. 14, 2022 from IEEE Xplore. [cited by applicant]
Prof. Bruce Jacob, “The RiSC-16 Instruction-Set Architecture,” ENEE 646: Digital Computer Design, Fall 2002. [cited by applicant]
Erik Buchanan, et al., “When Good Instructions Go Bad: Generalizing Return-Oriented Programming to RISC,” In Proceedings of the 15th ACM Conference on Computer and Communications Security, CCS'08, Oct. 2008. [cited by applicant]
J. R. Burch, et al., “Sequential Circuit Verification Using Symbolic Model Checking,” 27th ACM/IEEE Design Automation Conference, 1990 IEEE, downloaded on Mar. 14, 2022 from IEEE Xplore. [cited by applicant]
Stephen Checkoway, et al., “Return-Oriented Programming without Returns,” In Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS'10, Oct. 2010. [cited by applicant]
Hari Cherupalli, et al., “Bespoke Processors for Applications with Ultra-low Area and Power Constraints,” In Proceedings of ISCA '17, Jun. 2017. [cited by applicant]
Edmund Clarke, et al., “Hardware Verification using ANSI-C Programs as a Reference,” In Proceedings of the ASP-DAC Asia and South Pacific Design Automation Conference, 2003, pp. 308-311, 2003 IEEE. [cited by applicant]
Christopher Domas, “Breaking the x86 ISA,” Black Hat, Jul. 27, 2017. [cited by applicant]
Rolf Drechsler, “Synthesizing Checkers for On-Line Verification of System-On-Chip Designs,” In Proceedings of the 2003 International Symposium on Circuits and Systems, 2003, ISCAS'03, vol. 4, 2003 IEEE, downloaded on Ma… [cited by applicant]
Lieven Eeckhout, “Is Moore's Law Slowing Down? What's Next?,” From the Editor in Chief, IEEE Computer Society, www.computer.org/micro, Jul./Aug. 2017 IEEE. [cited by applicant]
Hadi Esmaeilzadeh, et al., “Dark Silicon and the End of Multicore Scaling,” IEEE Computer Society, IEEE Micro, May/Jun. 2012. [cited by applicant]
Paul Gastin, et al., “Fast LTL to Buchi Automata Translation,” In International Conference on Computer Aided Verification, CAV 2001, LNCS 2102, pp. 53-65, 2001. [cited by applicant]
Rich Goldman, et al., “IC Design Course Based on the Synopsys DesignWare ARC 600 Processor Core and 32/28nm Educational Design Kit,” In Fourth Interdisciplinary Engineering Design Education conference, IEDEC, 2013 IEEE,… [cited by applicant]
Ricardo Gonzalez, “Xtensa: A Configurable and Extensible Processor,” IEEE Micro, Mar.-Apr. 2000, downloaded on Mar. 14, 2022 from IEEE Xplore. [cited by applicant]
Daniel Grobe, et al., “HW/SW Co-Verification of Embedded Systems using Bounded Model Checking,” In Proceedings of the 16th ACM Great Lakes symposium on VLSI, pp. 43-48, GLSVLSI'06, 2006. [cited by applicant]
Matthew Guthaus, et al., “MiBench: A Free, commercially representative embedded benchmark suite,” In Proceedings of the fourth annual IEEE international workshop on workload characterization, pp. 3-14, 2001 IEEE, downlo… [cited by applicant]
Simon Hammond, et al., “Evaluating the Intel Skylake Xeon Processor for HPC Workloads,” 2018 International Conference on High Performance Computing & Simulation, 2018 IEEE, downloaded on Mar. 14, 2022 from IEEE Xplore. [cited by applicant]
Klaus Havelund, et al., “Synthesizing Monitors for Safety Properties,” In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2002, LNCS 2280, pp. 342-356, 2002. [cited by applicant]
Jiongrui He, et al., “High-performance RISC-V processor with improved dispatch and commit schemes,” In 2020 International Conference on Electronics, Information, and Communication (ICEIC), pp. 1-4. IEEE, 2020, downloade… [cited by applicant]
Matthew Hicks, et al., “SPECS: A Lightweight Runtime Mechanism for Protecting Software from Security-Critical Processor Bugs,” In Proceedings of the Twentieth International Conference on Architectural Support for Progra… [cited by applicant]
Mark Hill, et al., “On the Spectre and Meltdown Processor Security Vulnerabilities,” Theme Article, IEEE Computer Society, Mar./Apr. 2019, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
Evgeniy Ilyushin, et al., “On source-to-source compilers,” International Journal of Open Information Technologies International Journal of Open Information Technologies, 4(5), 2016. [cited by applicant]
Intel, “Desktop 3rd Generation Intel® Core ™ Processor Family, Specification Update,” Revision 022, Apr. 2016. [cited by applicant]
Intel, “Desktop 4th Generation Intel® Core™ Processor Family, Desktop Intel® Pentium® Processor Family, and Desktop Intel® Celeron® Processor Family, Specification Update,” Revision 039US, Apr. 2020. [cited by applicant]
Intel, 8th and 9th Generation Intel® Core™ Processor Family, Specification Update,' Revision 002, Nov. 2019. [cited by applicant]
“Intel® FPGA IP Portfolio,” FPGA IP (Intellectual Property) Cores—Intel® FPGA, 2020, https://www.intel.com/content/www.us.en/products/programmable/intellectual-property.html, printed from World Wide Web Mar. 15, 2022. [cited by applicant]
Kenta Ishiguro, et al., “Hardening Hypervisors against Vulnerabilities in Instruction,” In Proceedings of the 11th European Workshop on Systems Security, pp. 1-6, EuroSec'18, Apr. 2018. [cited by applicant]
Manoj Kumar Jain, et al., “ASIP Design Methodologies : Survey and Issues,” In VLSI Design 2001, Fourteenth International Conference on VLSI Design, pp. 76-81, 2001 IEEE, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
Paul Kocher, et al., “Spectre Attacks: Exploiting Speculative Execution,” 2019 IEEE Symposium on Security and Privacy, 2019 IEEE, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
Leslie Lamport, “What Good is Temporal Logic?,” Invited Paper, Information Processing 83, R.E.A. Mason (ed.), pp. 657-668, 1983. [cited by applicant]
F. J. Lin, et al., “Protocol Verification Using Reachability Analysis: The State Space Explosion Problem and Relief Strategies',” In Proceedings of the ACM Workshop on Frontiers in Computer Communications technology, 19… [cited by applicant]
Bruno Cardoso Lopes, et al., “SHRINK: Reducing the ISA Complexity Via Instruction Recycling,” ISA '15, Jun. 2015. [cited by applicant]
Bruno Lopes, et al., “ISA Aging: An X86 case study,” ResearchGate, Conference Paper, Jul. 2013. [cited by applicant]
“Ibex Documentation, Release 0.1.dev50+gf44ae90.d20220321, lowRIsC,” Ibex user Manual, Mar. 21, 2022. [cited by applicant]
Grant Martin, “Recent Developments in Configurable and Extensible Processors,” Architectures and Processors (ASAP'06), 2006 IEEE, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
K.L. McMillan, “A methodology for hardware verification using compositional model checking,” Science of Computer Programming 37, pp. 279-309, 2000. [cited by applicant]
“Questa Formal Verification Apps—Exhaustive Solutions for Verification Challenges,” https://eda.sw.siemens.com/en-US/ic/questa/formal-verification/, 2020, printed from the World Wide Web Mar. 15, 2022. [cited by applicant]
Atsushi Mizuno, et al., “Design Methodology and System for a Configurable Media Embedded Processor Extensible to VLIW Architecture,” Proceedings of the 2002 IEEE International Conference on Computer Design: VLSI in Comp… [cited by applicant]
Kris Myny, et al., “An 8-Bit, 40-Instructions-Per-Second Organic Microprocessor on Plastic Foil,” IEEE Journal of Solid-State Circuits, 2011 IEEE, Dec. 2011, downloaded on Mar. 15, 2022 from IEEE Xplore. [cited by applicant]
Hamid Noori, et al., “General Overview of an Adaptive Dynamic Extensible Processor,” In Workshop on Introspective Architectues, 2006. [cited by applicant]