Nothing Special   »   [go: up one dir, main page]

Guo et al., 2016 - Google Patents

Automatic RTL-to-formal code converter for IP security formal verification

Guo et al., 2016

View PDF
Document ID
14356576579054124736
Author
Guo X
Dutta R
Mishra P
Jin Y
Publication year
Publication venue
2016 17th International Workshop on Microprocessor and SOC Test and Verification (MTV)

External Links

Snippet

The wide usage of hardware intellectual property (IP) cores from untrusted vendors has raised security concerns in the integrated circuit (IC) industry. Existing testing methods are designed to validate the functionality of the hardware IP cores. These methods often fall …
Continue reading at www.jinyier.me (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/5022—Logic simulation, e.g. for logic circuit operation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5045—Circuit design
    • G06F17/505—Logic synthesis, e.g. technology mapping, optimisation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/57—Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities
    • G06F21/577—Assessing vulnerabilities and evaluating computer system security
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5068—Physical circuit design, e.g. layout for integrated circuits or printed circuit boards
    • G06F17/5081—Layout analysis, e.g. layout verification, design rule check
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/55—Detecting local intrusion or implementing counter-measures
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G06F8/43—Checking; Contextual analysis
    • G06F8/436—Semantic checking
    • G06F8/437—Type checking
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/70—Fault tolerant, i.e. transient fault suppression
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F7/00—Methods or arrangements for processing data by operating upon the order or content of the data handled
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2207/00—Indexing scheme relating to methods or arrangements for processing data by operating upon the order or content of the data handled
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2221/00—Indexing scheme relating to security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G—PHYSICS
    • G01—MEASURING; TESTING
    • G01R—MEASURING ELECTRIC VARIABLES; MEASURING MAGNETIC VARIABLES
    • G01R31/00—Arrangements for testing electric properties; Arrangements for locating electric faults; Arrangements for electrical testing characterised by what is being tested not provided for elsewhere
    • G01R31/28—Testing of electronic circuits, e.g. by signal tracer
    • G01R31/317—Testing of digital circuits
    • G01R31/3181—Functional testing
    • G01R31/3183—Generation of test inputs, e.g. test vectors, patterns or sequence

Similar Documents

Publication Publication Date Title
Farahmandi et al. System-on-chip security
Love et al. Proof-carrying hardware intellectual property: A pathway to trusted module acquisition
Guo et al. Scalable SoC trust verification using integrated theorem proving and model checking
Guo et al. Pre-silicon security verification and validation: A formal perspective
Love et al. Enhancing security via provably trustworthy hardware intellectual property
Boulé et al. Generating hardware assertion checkers
Jin et al. A proof-carrying based framework for trusted microprocessor IP
Kande et al. Llm-assisted generation of hardware assertions
US7971166B2 (en) Method, system, and program product for automated verification of gating logic using formal verification
Guo et al. Automatic code converter enhanced PCH framework for SoC trust verification
Paria et al. Divas: An llm-based end-to-end framework for soc security analysis and policy-based protection
Guo et al. Eliminating the hardware-software boundary: A proof-carrying approach for trust evaluation on computer systems
Whalen et al. Synthesizing certified code
Guo et al. Automatic RTL-to-formal code converter for IP security formal verification
Goli et al. Early SoCs Information Flow Policies Validation using SystemC-based Virtual Prototypes at the ESL
Akyash et al. Evolutionary large language models for hardware security: A comparative survey
Gadde et al. All artificial, less intelligence: Genai through the lens of formal verification
Guo et al. Hierarchy-preserving formal verification methods for pre-silicon security assurance
Jiang et al. PyH2: Using PyMTL3 to create productive and open-source hardware testing methodologies
Punnoose et al. Survey of Existing Tools for Formal Verification.
Borrione et al. PSL-based online monitoring of digital systems
Borrione et al. On-line assertion-based verification with proven correct monitors
Khan et al. VeriFormal: An executable formal model of a hardware description language
Li Formal methods for reverse engineering gate-level netlists
Jin EDA tools trust evaluation through security property proofs