[go: up one dir, main page]

GB2579919B - Detecting out-of-bounds violations in a hardware design using formal verification - Google Patents

Detecting out-of-bounds violations in a hardware design using formal verification Download PDF

Info

Publication number
GB2579919B
GB2579919B GB2000776.1A GB202000776A GB2579919B GB 2579919 B GB2579919 B GB 2579919B GB 202000776 A GB202000776 A GB 202000776A GB 2579919 B GB2579919 B GB 2579919B
Authority
GB
United Kingdom
Prior art keywords
hardware design
formal verification
detecting out
bounds violations
violations
Prior art date
Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
Active
Application number
GB2000776.1A
Other versions
GB2579919A (en
GB202000776D0 (en
Inventor
Singleton Iain
Darbari Ashish
Current Assignee (The listed assignees may be inaccurate. Google has not performed a legal analysis and makes no representation or warranty as to the accuracy of the list.)
Imagination Technologies Ltd
Original Assignee
Imagination Technologies Ltd
Priority date (The priority date is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the date listed.)
Filing date
Publication date
Application filed by Imagination Technologies Ltd filed Critical Imagination Technologies Ltd
Priority to GB2000776.1A priority Critical patent/GB2579919B/en
Priority claimed from GB1617531.7A external-priority patent/GB2554941B/en
Publication of GB202000776D0 publication Critical patent/GB202000776D0/en
Publication of GB2579919A publication Critical patent/GB2579919A/en
Application granted granted Critical
Publication of GB2579919B publication Critical patent/GB2579919B/en
Active legal-status Critical Current
Anticipated expiration legal-status Critical

Links

Classifications

    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F30/00—Computer-aided design [CAD]
    • G06F30/30—Circuit design
    • G06F30/39—Circuit design at the physical level
    • G06F30/398—Design verification or optimisation, e.g. using design rule check [DRC], layout versus schematics [LVS] or finite element methods [FEM]
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F30/00—Computer-aided design [CAD]
    • G06F30/30—Circuit design
    • G06F30/32—Circuit design at the digital level
    • G06F30/33—Design verification, e.g. functional simulation or model checking
    • G06F30/3323—Design verification, e.g. functional simulation or model checking using formal methods, e.g. equivalence checking or property checking
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F12/00—Accessing, addressing or allocating within memory systems or architectures
    • G06F12/14—Protection against unauthorised use of memory or access to memory
    • G06F12/1458—Protection against unauthorised use of memory or access to memory by checking the subject access rights
    • G06F12/1491—Protection against unauthorised use of memory or access to memory by checking the subject access rights in a hierarchical protection system, e.g. privilege levels, memory rings
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC 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/575—Secure boot
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/70—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer
    • G06F21/71—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer to assure secure computing or processing of information
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/70—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer
    • G06F21/71—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer to assure secure computing or processing of information
    • G06F21/74—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer to assure secure computing or processing of information operating in dual or compartmented mode, i.e. at least one secure mode

Landscapes

  • Engineering & Computer Science (AREA)
  • Theoretical Computer Science (AREA)
  • Computer Hardware Design (AREA)
  • Physics & Mathematics (AREA)
  • General Engineering & Computer Science (AREA)
  • Computer Security & Cryptography (AREA)
  • General Physics & Mathematics (AREA)
  • Software Systems (AREA)
  • Mathematical Physics (AREA)
  • Evolutionary Computation (AREA)
  • Geometry (AREA)
  • Debugging And Monitoring (AREA)
GB2000776.1A 2016-10-14 2016-10-14 Detecting out-of-bounds violations in a hardware design using formal verification Active GB2579919B (en)

Priority Applications (1)

Application Number Priority Date Filing Date Title
GB2000776.1A GB2579919B (en) 2016-10-14 2016-10-14 Detecting out-of-bounds violations in a hardware design using formal verification

Applications Claiming Priority (2)

Application Number Priority Date Filing Date Title
GB1617531.7A GB2554941B (en) 2016-10-14 2016-10-14 Detecting out-of-bounds violations in a hardware design using formal verification
GB2000776.1A GB2579919B (en) 2016-10-14 2016-10-14 Detecting out-of-bounds violations in a hardware design using formal verification

Publications (3)

Publication Number Publication Date
GB202000776D0 GB202000776D0 (en) 2020-03-04
GB2579919A GB2579919A (en) 2020-07-08
GB2579919B true GB2579919B (en) 2021-04-07

Family

ID=69637035

Family Applications (1)

Application Number Title Priority Date Filing Date
GB2000776.1A Active GB2579919B (en) 2016-10-14 2016-10-14 Detecting out-of-bounds violations in a hardware design using formal verification

Country Status (1)

Country Link
GB (1) GB2579919B (en)

Citations (2)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US20030018461A1 (en) * 2001-07-16 2003-01-23 International Business Machines Corporation Simulation monitors based on temporal formulas
EP1329787A2 (en) * 2002-01-16 2003-07-23 Texas Instruments Incorporated Secure mode indicator for smart phone or PDA

Patent Citations (2)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US20030018461A1 (en) * 2001-07-16 2003-01-23 International Business Machines Corporation Simulation monitors based on temporal formulas
EP1329787A2 (en) * 2002-01-16 2003-07-23 Texas Instruments Incorporated Secure mode indicator for smart phone or PDA

Also Published As

Publication number Publication date
GB2579919A (en) 2020-07-08
GB202000776D0 (en) 2020-03-04

Similar Documents

Publication Publication Date Title
GB2554941B (en) Detecting out-of-bounds violations in a hardware design using formal verification
GB2519181B (en) Clock verification
GB2546603B (en) Arbiter verification
GB2551524B (en) Livelock detection in a hardware design using formal verification
EP3103084A4 (en) Token verification using limited use certificates
IL252144A0 (en) Training in dispensing a medicament
SG11201608973TA (en) Data verification using access device
IL259479B (en) Cancer treatment using 2-deoxy-2-fluoro-l-fucose in combination with a checkpoint inhibitor
GB201517416D0 (en) Task-execution in a DBMS using stored procedures
GB201411023D0 (en) Read assist techniques in a memory device
GB201420116D0 (en) Verifying a graph-based coherency verification tool
GB2549280B (en) Self-testing in a processor core
PL2985477T3 (en) Fastening device and fastening assembly, in particular for fastening a sanitary object
GB201516617D0 (en) Verification for payment transations
PL3180527T3 (en) Fastening device and fastening assembly, in particular for fastening a sanitary object
DK3138593T3 (en) Valve coupling device and metering unit with a valve coupling device
IL254146A (en) Solid-joint deformation-model verification
PL3147434T3 (en) Drive device for a lock, in particular for a stand wing lock
GB201718282D0 (en) Ball seat for use in a wellbore
GB201501086D0 (en) User Verification
GB201507019D0 (en) A security device
PL3280500T3 (en) System for counting scores in a sports match
GB2541962B (en) Identifying bugs in a counter using formal
GB201712422D0 (en) Method for authenticating a user at a security device
GB2579919B (en) Detecting out-of-bounds violations in a hardware design using formal verification

Legal Events

Date Code Title Description
732E Amendments to the register in respect of changes of name or changes affecting rights (sect. 32/1977)

Free format text: REGISTERED BETWEEN 20240822 AND 20240828