Articles by Ashish
-
Exhaustive Formal Verification of Packet Based Designs
Exhaustive Formal Verification of Packet Based Designs
By Ashish Darbari
Activity
-
Hot Chips Symposium 2024. Day one impressions... First keynote by OpenAI. Very clear message: scaling laws tell us to keep pushing believe in…
Hot Chips Symposium 2024. Day one impressions... First keynote by OpenAI. Very clear message: scaling laws tell us to keep pushing believe in…
Liked by Ashish Darbari
-
🚀 𝗝𝗼𝗶𝗻 𝗨𝘀 𝗮𝘁 𝗗𝗩𝗖𝗼𝗻 𝗜𝗻𝗱𝗶𝗮 𝟮𝟬𝟮𝟰 𝘁𝗼 𝗛𝗲𝗮𝗿 𝗛𝗮𝗿𝗿𝘆 𝗙𝗼𝘀𝘁𝗲𝗿! 🚀 We are thrilled to invite you to attend Harry…
🚀 𝗝𝗼𝗶𝗻 𝗨𝘀 𝗮𝘁 𝗗𝗩𝗖𝗼𝗻 𝗜𝗻𝗱𝗶𝗮 𝟮𝟬𝟮𝟰 𝘁𝗼 𝗛𝗲𝗮𝗿 𝗛𝗮𝗿𝗿𝘆 𝗙𝗼𝘀𝘁𝗲𝗿! 🚀 We are thrilled to invite you to attend Harry…
Liked by Ashish Darbari
Experience
Education
-
University of Oxford
-
Activities and Societies: Co-founder Oxford Indian Society, Aug 2003. Charitable event organization. Local organizer TPHOLs 2005 conference in Oxford.
Thesis title: Symmetry Reduction for STE Model Checking using Structured Models
-
-
Thesis title: First-Order Rule Learning through Pulsed Neural Network. Thesis awarded 1.1(excellent),
-
-
Activities and Societies: IEEE Local chapter Treasurer. Organizer of the UNNAYAN 1997 event.
Thesis title: Fuzzy Intelligent Power Frequency Identification. Thesis awarded excellent ‘A’
Publications
-
Using formal methods to eradicate the last bug: Lessons learned from nature
Keynote at Intel India Technologists Day - Formal Verification Charter Session 4
-
Architectural verification and deadlocks
Axiomise Podcast
In this podcast, Dr. Darbari discusses architectural formal verification and deadlocks in processors. Deadlocks can cause all sorts of issues in the design and though you may believe that reset would be a great way of bringing the chip out of the deadlock, your customers may not want to always reboot the device. Use Axiomise formalISA to find & fix deadlocks and if you like prove that they have been fixed.
-
Everything you wanted to know about architectural formal verification
Axiomise Podcast
Dr. Darbari demystifies the topic of architectural formal verification with the focus on RISC-V. He describes the similarities with simulation-based compliance testing and key benefits of using formalISA and formal verification for architectural compliance. A brand-new blog on this topic is available from Tech Design Forums.
-
Using formal to vaccinate RISC-V designs against catastrophic bugs
RISC-V Global Forum
Bug escapes in silicon lead to catastrophic failures – well-known being the Intel FDIV bug, Ariane 5 explosion, and several ongoing security vulnerabilities affecting almost all the computing devices.
Formal verification provides exhaustive proofs of bug absence, as well as efficient bug-hunting. The use of formal methods in chip designs prevents bugs to creep in ensuring the chips remain clean, not exhibiting any symptoms of bugs – almost the same way as humans react when they are…Bug escapes in silicon lead to catastrophic failures – well-known being the Intel FDIV bug, Ariane 5 explosion, and several ongoing security vulnerabilities affecting almost all the computing devices.
Formal verification provides exhaustive proofs of bug absence, as well as efficient bug-hunting. The use of formal methods in chip designs prevents bugs to creep in ensuring the chips remain clean, not exhibiting any symptoms of bugs – almost the same way as humans react when they are vaccinated against life-threatening bugs.
So, is "formal verification" the vaccine that chip design needs to keep itself safe from bugs? Dr. Darbari believes it is. In this talk, he presents a methodology and an APP that can be used to find bugs both in designs-under-development and in pre-verified processors. The methodology shown is able to prove the bug absence using any formal verification tool. -
Universal formal verification for RISC-V processors
Design Automation Conference, IP Track
-
How is Axiomise making formal normal?
Axiomise Podcast
How is Axiomise is making formal normal? Listen in to Dr. Darbari to see how by combining training, and custom formal verification solutions Axiomise is enabling the industry in the use of formal methods. He talks about formalISA, a new app launched this week, and how it is able to obtain proofs, bugs, and coverage for establishing ISA compliance for RISC-V processors without writing a single line of verification code.
-
RISC-V formal verification for ISA compliance
Webinar hosted by Synopsys
RISC-V is an open standard instruction set architecture. It has experienced exponential growth in recent years, enabling users to design custom processors more quickly and cost effectively to meet today’s demand for more technological innovations in the CPU, GPU, AI, ML spaces.
However, verification of the processor to find all corner-case bugs from the architectural and microarchitectural levels pose a tremendous challenge for dynamic simulation and emulation. Formal verification is…RISC-V is an open standard instruction set architecture. It has experienced exponential growth in recent years, enabling users to design custom processors more quickly and cost effectively to meet today’s demand for more technological innovations in the CPU, GPU, AI, ML spaces.
However, verification of the processor to find all corner-case bugs from the architectural and microarchitectural levels pose a tremendous challenge for dynamic simulation and emulation. Formal verification is known for its ability to prove the absence of bugs as well as find those complex corner-case bugs.
In this webinar, we will present a solution powered by a unique combination of Synopsys VC Formal apps and Axiomise’s RISC-V ISA formal solution enabling fast corner-case bug hunting, and exhaustive proofs of bug absence obtaining ISA compliance for RISC-V.
-
Ten reasons to use formal verification
In this podcast, Dr. Ashish Darbari outlines the ten reasons why formal verification should be used. Save money, find more bugs, find bugs quicker, prove bug absence, ship safe and secure chips.
-
Using formal verification to vaccinate chips against catastrophic bugs
Keynote at the Online International Conference on Advances in Physical, Mathematical and Computational Sciences.
Dr. Ashish Darbari, describes how to use formal verification to vaccinate chips against catstrophic bugs. This was a keynote talk given on 12 June 2020 in the Online International Conference on Advances in Physical, Mathematical and Computational Sciences.
-
Have you got it covered with formal verification?
In this podcast, Dr. Darbari talks about the connection between constraints and coverage in formal verification. He discusses why the two topics are closely connected using the concepts of controllability and observability and why proof-core and COI coverage are not the best mechanisms to sign-off formal verification, especially for inconclusive proofs.
-
Finding corner-case bugs in processors using architectural formal verification
Axiomise Podcast
What happens when you apply formal verification to find architectural flaws in processors? In this podcast, Dr. Ashish Darbari talks about an interesting way of using Axiomise ISA formal proof kit to find bugs in RISC-V cores. He describes how by using the combination of automated formal properties from the Axiomise proof kit together with constraints we can not only find bugs but also root-cause the precise nature of simulation resistant bugs. You might like this podcast if you ever wondered…
What happens when you apply formal verification to find architectural flaws in processors? In this podcast, Dr. Ashish Darbari talks about an interesting way of using Axiomise ISA formal proof kit to find bugs in RISC-V cores. He describes how by using the combination of automated formal properties from the Axiomise proof kit together with constraints we can not only find bugs but also root-cause the precise nature of simulation resistant bugs. You might like this podcast if you ever wondered how constraints together with automated formal can be used to address the complex challenges of finding corner-case bugs in your CPU designs.
-
Role of constraints in formal verification
Axiomise Podcast
In this podcast, we discuss the role of constraints in formal verification. One of the biggest challenges with formal verification is scoping out what constraints are needed, and how they will be coded in formal verification for efficient predictable results.
-
Why coverage is important for formal verification?
Axiomise Podcast
We answer why coverage is important for formal verification and sign-off. We examine why coverage is important and what can be done to sign-off the verification with confidence. We discuss the interaction between structural coverage, functional coverage in simulation, and what happens for formal verification, and what should happen?
-
Role of specifications in verification
Axiomise Podcast
In this podcast, Dr. Darbari talks about the role of specifications in verification. Requirements & specifications play a very important part in establishing what can be obtained from a verification task. The general rule is if it ain't specified it won't be verified. After all, any testing & verification exercise needs to know what is being tested, and what is expected from a test?
-
Key drivers for maximizing verification ROI
Axiomise Podcast
We describe what are the key factors to maximize verification ROI, focusing on Axiomise formal verification and how we can improve the return-on-investment.
-
Why processors need formal verification?
Axiomise Podcast
Dr. Darbari talks about why processors need formal verification in the latest podcast. He describes why processors are complex, and why formal verification is a necessity.
-
History of formal methods
Axiomise Podcast
In this podcast, we cover the rich history of formal methods, explaining the basics of formal verification covering theorem proving, model checking and equivalence checking. We explain why formal verification is perceived to be hard. We make formal verification easier!
-
Basics of testing and formal verification for SoCs
Axiomise Podcast
In this podcast, Dr Ashish Darbari talks about testing and formal verification for SoCs. He describes the basics of simulation-based-verification techniques such as constrained random verification, directed testing, emulation, and formal verification. Subscribe to our youtube channel and our newsletters at axiomise.com. Ping us at [email protected] with your suggestions, questions, and feedback.
-
A 30,000 ft introduction to a system-on-chip
Axiomise Podcast
In this podcast, Dr Ashish Darbari presents a 30,000 ft introduction to a system-on-chip (SoC) and the numerous test and formal verification challenges that affect the design of these ubiquitous components that almost everyone on the planet owns!
-
How to make formal verification scalable and predictable?
Synopsys VC Formal SIG Invited Talk
-
Smart Formal for Scalable Verification
DVCon USA
-
Efficient Formal Verification with Smart Modelling
Synopsys/Axiomise Webinar
-
Formal verification of low-power RISC-V processors
DVCon India
-
Exhaustive Formal Verification of Packet-based Designs
Synopsys/Axiomise Webinar
-
It’s about Time: Verifying Clocks with Formal
Design Automation Conference
-
Abstraction: The Universal Formal Verification App
Proceedings of the Cadence Jasper User Group
-
The Ten Myths About Formal
Keynote Talk in the 3rd Formal Verification Conference UK
-
Stretch Your Imagination From Validation to Verification using Formal Methods
2nd Formal Verification Conference
-
Using STE for Requirements Modelling and Design Verification
Technical Report
-
Symbolic Simulation based Transient Fault Injection Methodology
Technical Report University of Southampton
-
A Correct-by-Construction Methodology for Designing Symmetric Circuits
International Symmetry Conference
-
A Structured Modelling Framework for Capturing Symmetry in Circuits
13th Automated Reasoning Workshop
-
Symmetry Reduction for STE Model Checking
6th Formal Methods in Computer Aided Design
-
Formalization and Execution of STE in HOL
Supplementary Proceedings of the 16th International Conference in Theorem Proving in Higher Order Logics (TPHOLS),
-
Formalization and Execution of STE in HOL (Extended Version)
Technical Report Oxford University
-
Rule Extraction from Trained ANN: A Survey
Technical Report, TU Dresden
-
Scenario coverage in formal verification
-
Dr. Darbari talks about a new coverage solution for formal verification called scenario coverage. He describes why you need it, what it is, and how this has been used to verify the latest core from the OpenHW group - CVE4. Let's cover our formal verification properly.
-
Six dimensions of coverage for formal verification
Axiomise Podcast
Learn how to sign-off formal verification using six dimensions of coverage. Metric-driven verification is important, but we need to consider all aspects when using formal verification including qualitative and quantitative methods. We made it easy for you to use the six dimensions of coverage to sign-off RISC-V verification. Find out about it in more detail next week at the RISC-V summit.
Patents
-
Verifying firmware binary images using a hardware design and formal assertions
Issued 11989299
Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include…
Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more assertions that assert that if a stop of firmware execution has been detected, that a decode of an illegal firmware instruction has (or has not) been detected.
-
Formal verification tool to verify hardware design of memory unit
Issued 11948652
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic…
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic read is a read of the symbolic address. The hardware monitors also include assertion verification logic that verifies an assertion that read data corresponding to a symbolic reads matches write data associated with one or more symbolic writes preceding the read.
Other inventors -
Livelock recovery circuit for detecting illegal repetition of an instruction and transitioning to a known state
Issued 11847456
Livelock recovery circuits configured to detect livelock in a processor, and cause the processor to transition to a known safe state when livelock is detected. The livelock recovery circuits include detection logic configured to detect that the processor is in livelock when the processor has illegally repeated an instruction; and transition logic configured to cause the processor to transition to a safe state when livelock has been detected by the detection logic.
-
Detecting out-of-bounds violations in a hardware design using formal verification
Issued 11663386
A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory…
A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory address of the fetched instruction to an allowable memory address range associated with the current operating state of the instantiation of the hardware design to determine whether there has been an out-of-bounds violation. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design does not cause an instruction to be fetched from an out-of-bounds address.
Other inventors -
Out of bounds recovery circuit
Issued 11593193
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating…
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating state of the electronic device; and transition logic configured to cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation has been detected by the detection logic.
Other inventors -
Assessing performance of a hardware design using formal evaluation logic
Issued US-11531799-B2
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the hardware design to detect whether the hardware design is in a livelock comprising the…
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the hardware design to detect whether the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design cannot enter a livelock comprising the predetermined state.
Other inventors -
Control path verification of hardware design for pipelined process
Issued US-11475193-B2
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an…
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an assertion based language, the assertion establishing that when the watched data is output from the pipelined process the counted number of progressing clock cycles for the watched data should be equal to one of one or more predetermined values.
-
Livelock recovery circuit for detecting illegal repetition of an instruction and transitioning to a known state
Issued US-11467840-B2
Livelock recovery circuits configured to detect livelock in a processor, and cause the processor to transition to a known safe state when livelock is detected. The livelock recovery circuits include detection logic configured to detect that the processor is in livelock when the processor has illegally repeated an instruction; and transition logic configured to cause the processor to transition to a safe state when livelock has been detected by the detection logic.
Other inventors -
Livelock detection in a hardware design using formal evaluation logic
Issued US11373025B2
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the…
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the instantiation of the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the instantiation of the hardware design cannot enter a livelock comprising the predetermined state.
Other inventors -
Detecting out-of-bounds violations in a hardware design using formal verification
Issued US-11250192-B2
A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory…
A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory address of the fetched instruction to an allowable memory address range associated with the current operating state of the instantiation of the hardware design to determine whether there has been an out-of-bounds violation. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design does not cause an instruction to be fetched from an out-of-bounds address.
Other inventors -
Formal verification tool to verify hardware design of memory unit
Issued US-11250927-B2
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic…
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic read is a read of the symbolic address. The hardware monitors also include assertion verification logic that verifies an assertion that read data corresponding to a symbolic reads matches write data associated with one or more symbolic writes preceding the read.
Other inventors -
Identifying bugs in a counter using formal
Issued EP-3408768-B1
-
Out-of-bounds recovery circuit
Issued US 11030039
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating…
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating state of the electronic device; and transition logic configured to cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation has been detected by the detection logic.
Other inventors -
Verifying firmware binary images using a hardware design and formal assertions
Issued US 11010477
Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include…
Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more assertions that assert that if a stop of firmware execution has been detected, that a decode of an illegal firmware instruction has (or has not) been detected. The hardware monitor may be used by a formal verification tool to exhaustively verify that the firmware boot image does not comprise an illegal firmware instruction, or during simulation to detect illegal firmware instructions in a firmware boot image.
-
Detecting out-of-bounds violations in a hardware design using formal verification
Issued GB-2579919-B
-
Out-of-bounds recovery circuit
Issued GB-2579918-B
-
Assessing performance of a hardware design using formal evaluation logic
Issued US 10963611
A hardware monitor arranged to assess the performance of a hardware design for an integrated circuit to complete a task. The hardware monitor includes monitoring and counting logic configured to count a number of cycles between start and completion of the symbolic task in the hardware design; and property evaluation logic configured to evaluate one or more formal properties related to the counted number of cycles to assess the performance of the hardware design in completing the symbolic task…
A hardware monitor arranged to assess the performance of a hardware design for an integrated circuit to complete a task. The hardware monitor includes monitoring and counting logic configured to count a number of cycles between start and completion of the symbolic task in the hardware design; and property evaluation logic configured to evaluate one or more formal properties related to the counted number of cycles to assess the performance of the hardware design in completing the symbolic task. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design meets a desired performance goal and/or to exhaustively identify a performance metric (e.g. best case and/or worst case performance) with respect to completion of the task.
Other inventors -
Control path verification of hardware design for pipelined process
Issued US 10949590
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an…
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an assertion based language, the assertion establishing that when the watched data is output from the pipelined process the counted number of progressing clock cycles for the watched data should be equal to one of one or more predetermined values.
-
Detecting out-of-bounds violations in a hardware design using formal verification
Issued US-10936775-B2
-
Clock Verification
Issued US 10929583
Methods and systems for verifying a derived clock using assertion-based verification. The method comprises counting the number of full or half cycles of a fast clock that occur between the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow clock); counting the number of full or half cycles of the fast clock that occur between the falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow clock); and verifying the counts using…
Methods and systems for verifying a derived clock using assertion-based verification. The method comprises counting the number of full or half cycles of a fast clock that occur between the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow clock); counting the number of full or half cycles of the fast clock that occur between the falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow clock); and verifying the counts using assertion-based verification.
-
Livelock detection in a hardware design using formal evaluation logic
Issued US 10909289
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the…
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the instantiation of the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the instantiation of the hardware design cannot enter a livelock comprising the predetermined state.
-
Out-of-bounds recovery circuit
Issued US 10817367
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating…
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating state of the electronic device; and transition logic configured to cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation has been detected by the detection logic.
Other inventorsSee patent -
Assessing performance of a hardware design using formal verification
Issued EP-3249535-B1
-
Dynamic power measurement using formal verification
Issued EP-3193236-B1
-
Detecting out-of-bounds violations in a hardware design using formal verification
Issued US 10755011
A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory…
A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory address of the fetched instruction to an allowable memory address range associated with the current operating state of the instantiation of the hardware design to determine whether there has been an out-of-bounds violation. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design does not cause an instruction to be fetched from an out-of-bounds address.
-
Detecting out-of-bounds violations in a hardware design using formal verification
Issued GB-2554941-B
-
Out-of-bounds recovery circuit
Issued GB GB2554940A
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating…
Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating state of the electronic device; and transition logic configured to cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation has been detected by the detection logic.
Other inventors -
Hardware monitor to verify memory units
Issued US US10580511B2
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic…
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic read is a read of the symbolic address. The hardware monitors also include assertion verification logic that verifies an assertion that read data corresponding to a symbolic reads matches write data associated with one or more symbolic writes preceding the read.
Other inventorsSee patent -
Livelock recovery circuit configured to detect illegal repetition of an instruction and transition to a known state
Issued US 10,552,155
Livelock recovery circuits configured to detect livelock in a processor, and cause the processor to transition to a known safe state when livelock is detected. The livelock recovery circuits include detection logic configured to detect that the processor is in livelock when the processor has illegally repeated an instruction; and transition logic configured to cause the processor to transition to a safe state when livelock has been detected by the detection logic.
Other inventorsSee patent -
Identifying bugs in a counter using formal
Issued GB GB2541962
A method of detecting a bug in a counter of a hardware design that includes formally verifying, using a formal verification tool, an inductive assertion from a non-reset state of an instantiation of the hardware design. The inductive assertion establishes a relationship between the counter and a test bench counter at two or more points in time. If the formal verification tool identifies at least one valid state of an instantiation of the counter in which the inductive assertion is not true…
A method of detecting a bug in a counter of a hardware design that includes formally verifying, using a formal verification tool, an inductive assertion from a non-reset state of an instantiation of the hardware design. The inductive assertion establishes a relationship between the counter and a test bench counter at two or more points in time. If the formal verification tool identifies at least one valid state of an instantiation of the counter in which the inductive assertion is not true, information is output indicating a location of a bug in the hardware design or the test bench counter.
-
Hardware Monitor to Verify Memory Units
Issued GB GB2542214
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic…
Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic read is a read of the symbolic address. The hardware monitors also include assertion verification logic that verifies an assertion that read data corresponding to a symbolic reads matches write data associated with one or more symbolic writes preceding the read.
Other inventors -
Clock Verification
Issued US 10366187
Methods and systems for verifying a derived clock using assertion-based verification. The method comprises counting the number of full or half cycles of a fast clock that occur between the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow clock); counting the number of full or half cycles of the fast clock that occur between the falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow clock); and verifying the counts using…
Methods and systems for verifying a derived clock using assertion-based verification. The method comprises counting the number of full or half cycles of a fast clock that occur between the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow clock); counting the number of full or half cycles of the fast clock that occur between the falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow clock); and verifying the counts using assertion-based verification.
-
Dynamic power measurement using a formal verification tool
Issued US 10359825
Methods, systems and hardware monitors for verifying that an integrated circuit defined by a hardware design meets a power requirement including detecting whether a power consuming transition has occurred for one or more flip-flops of an instantiation of the hardware design; in response to detecting that a power consuming transition has occurred, updating a count of power consuming transitions for the instantiation of the hardware design; and determining, whether the power requirement is met at…
Methods, systems and hardware monitors for verifying that an integrated circuit defined by a hardware design meets a power requirement including detecting whether a power consuming transition has occurred for one or more flip-flops of an instantiation of the hardware design; in response to detecting that a power consuming transition has occurred, updating a count of power consuming transitions for the instantiation of the hardware design; and determining, whether the power requirement is met at a particular point in time by evaluating one or more properties that are based on the count of power consuming transitions.
Other inventors -
Livelock detection in a hardware design using formal evaluation logic
Issued US 10346571
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the…
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the instantiation of the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the instantiation of the hardware design cannot enter a livelock comprising the predetermined state.
-
Livelock recovery circuit
Issued GB GB2551523A
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the…
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to detect whether the instantiation of the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the instantiation of the hardware design cannot enter a livelock comprising the predetermined state.
Other inventors -
Assessing performance of a hardware design using formal evaluation logic
Issued US 10331831
A hardware monitor arranged to assess performance of a hardware design for an integrated circuit to complete a task. The hardware monitor includes monitoring and counting logic configured to count a number of cycles between start and completion of the symbolic task in an instantiation of the hardware design; and property evaluation logic configured to evaluate one or more formal properties related to the counted number of cycles to assess the performance of the instantiation of the hardware…
A hardware monitor arranged to assess performance of a hardware design for an integrated circuit to complete a task. The hardware monitor includes monitoring and counting logic configured to count a number of cycles between start and completion of the symbolic task in an instantiation of the hardware design; and property evaluation logic configured to evaluate one or more formal properties related to the counted number of cycles to assess the performance of the instantiation of the hardware design in completing the symbolic task. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design meets a desired performance goal and/or to exhaustively identify a performance metric (e.g. best case and/or worst case performance) with respect to completion of the task.
-
Control path verification of hardware design for pipelined process
Issued US 10325044
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an…
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an assertion based language, the assertion establishing that when the watched data is output from the pipelined process the counted number of progressing clock cycles for the watched data should be equal to one of one or more predetermined values.
Other inventors -
Control path verification of hardware design for pipelined process
Issued GB 2561299B
-
Arbiter Verification
Issued US 10210119
Operation of an arbiter in a hardware design is verified. The arbiter receives a plurality of requests over a plurality of clock cycles, including a monitored request and outputs the requests in priority order. The requests received by and output from the arbiter in each clock cycle are identified. The priority of the watched request relative to other pending requests in the arbiter is then tracked using a counter that is updated based on the requests input to and output from the arbiter in…
Operation of an arbiter in a hardware design is verified. The arbiter receives a plurality of requests over a plurality of clock cycles, including a monitored request and outputs the requests in priority order. The requests received by and output from the arbiter in each clock cycle are identified. The priority of the watched request relative to other pending requests in the arbiter is then tracked using a counter that is updated based on the requests input to and output from the arbiter in each clock cycle and a mask identifying the relative priority of requests received by the arbiter in the same clock cycle. The operation of the arbiter is verified using an assertion which establishes a relationship between the counter and the clock cycle in which the watched request is output from the arbiter.
Other inventors -
Verifying firmware binary images using a hardware design and formal assertions
Issued GB GB2554942
Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include…
Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more assertions that assert that if a stop of firmware execution has been detected, that a decode of an illegal firmware instruction has (or has not) been detected. The hardware monitor may be used by a formal verification tool to exhaustively verify that the firmware boot image does not comprise an illegal firmware instruction, or during simulation to detect illegal firmware instructions in a firmware boot image.
-
Identifying bugs in a counter using formal
Issued US 10108768
A method of detecting a bug in a counter of a hardware design that includes formally verifying , using a formal verification tool , an inductive assertion from a non-reset state of an instantiation of the hardware design . The inductive assertion establishes a relationship between the counter and a test bench counter at two or more points in time . If the formal verification tool identifies at least one valid state of an instantiation of the counter in which the inductive assertion is not true…
A method of detecting a bug in a counter of a hardware design that includes formally verifying , using a formal verification tool , an inductive assertion from a non-reset state of an instantiation of the hardware design . The inductive assertion establishes a relationship between the counter and a test bench counter at two or more points in time . If the formal verification tool identifies at least one valid state of an instantiation of the counter in which the inductive assertion is not true , information is output indicating a location of a bug in the hardware design or the test bench counter.
-
Hardware data structure for tracking ordered transactions
Issued US-10089138-B2
-
Deadlock detection in hardware design using assertion based verification
Issued US-10083262-B2
-
Hardware data structure for tracking partially ordered and reordered transactions
Issued US 10067896B2
Methods and hardware data structures are provided for tracking ordered transactions in a multi-transactional hardware design comprising one or more slaves configured to receive transaction requests from a plurality of masters. The data structure includes one or more counters for keeping track of the number of in-flight transactions; a table that keeps track of the age of each of the in-flight transactions for each master using the one or more counters; and control logic that verifies that a…
Methods and hardware data structures are provided for tracking ordered transactions in a multi-transactional hardware design comprising one or more slaves configured to receive transaction requests from a plurality of masters. The data structure includes one or more counters for keeping track of the number of in-flight transactions; a table that keeps track of the age of each of the in-flight transactions for each master using the one or more counters; and control logic that verifies that a transaction response for an in-flight transaction for a particular master has been issued by the slave in a predetermined order based on the tracked age for the in-flight transaction in the table.
-
Livelock detection in a hardware design using formal verification
Issued GB GB2551524
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the hardware design to detect whether the hardware design is in a livelock comprising the…
A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the hardware design to detect whether the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design cannot enter a livelock comprising the predetermined state.
Other inventors -
Control path verification of hardware design for pipelined process
Issued GB-2537939-B
-
Control path verification of hardware design for pipelined process
Issued GB GB2537939
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an…
Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an assertion based language, the assertion establishing that when the watched data is output from the pipelined process the counted number of progressing clock cycles for the watched data is equal to one or more predetermined number of clock cycles.
-
Dynamic power measurement using a formal verification tool
Issued GB GB2542215
Methods, systems and hardware monitors for verifying that an integrated circuit defined by a hardware design meets a power requirement including detecting whether a power consuming transition has occurred for one or more flip-flops of the hardware design; in response to detecting that a power consuming transition has occurred, updating a count of power consuming transitions for the hardware design; and determining, whether a power requirement is met at a particular point in time by evaluating…
Methods, systems and hardware monitors for verifying that an integrated circuit defined by a hardware design meets a power requirement including detecting whether a power consuming transition has occurred for one or more flip-flops of the hardware design; in response to detecting that a power consuming transition has occurred, updating a count of power consuming transitions for the hardware design; and determining, whether a power requirement is met at a particular point in time by evaluating one or more properties that are based on the count of power consuming transitions.
Other inventors -
Deadlock detection in hardware design using assertion based verification
Issued US US9767236B2
Methods and systems for detecting deadlock in a hardware design. The method comprises identifying one or more control signals in the hardware design; generating a state machine for each of the one or more control signals to track the state of the control signal; generating one or more assertions for each control signal to detect that the control signal is in a deadlock state from the state machine; and detecting whether any of the one or more control signal are in a deadlock state using the…
Methods and systems for detecting deadlock in a hardware design. The method comprises identifying one or more control signals in the hardware design; generating a state machine for each of the one or more control signals to track the state of the control signal; generating one or more assertions for each control signal to detect that the control signal is in a deadlock state from the state machine; and detecting whether any of the one or more control signal are in a deadlock state using the assertions. The method may also comprise generating one or more fairness constraints to impose on a particular assertion and detecting the particular control signal is in the deadlock state using the assertions under the fairness constraints.
Other inventors -
Hardware data structure for tracking partially ordered and reordered transactions
Issued US US9767057
Methods and hardware data structures are provided for tracking ordered transactions in a multi-transactional hardware design comprising one or more slaves configured to receive transaction requests from a plurality of masters. The data structure includes one or more counters for keeping track of the number of in-flight transactions; a table that keeps track of the age of each of the in-flight transactions for each master using the one or more counters; and control logic that verifies that a…
Methods and hardware data structures are provided for tracking ordered transactions in a multi-transactional hardware design comprising one or more slaves configured to receive transaction requests from a plurality of masters. The data structure includes one or more counters for keeping track of the number of in-flight transactions; a table that keeps track of the age of each of the in-flight transactions for each master using the one or more counters; and control logic that verifies that a transaction response for an in-flight transaction for a particular master has been issued by the slave in a predetermined order based on the tracked age for the in-flight transaction in the table.
-
Arbiter Verification
Issued US 9,626,465
Operation of an arbiter in a hardware design is verified. The arbiter receives a plurality of requests over a plurality of clock cycles, including a monitored request and outputs the requests in priority order. The requests received by and output from the arbiter in each clock cycle are identified. The priority of the watched request relative to other pending requests in the arbiter is then tracked using a counter that is updated based on the requests input to and output from the arbiter in…
Operation of an arbiter in a hardware design is verified. The arbiter receives a plurality of requests over a plurality of clock cycles, including a monitored request and outputs the requests in priority order. The requests received by and output from the arbiter in each clock cycle are identified. The priority of the watched request relative to other pending requests in the arbiter is then tracked using a counter that is updated based on the requests input to and output from the arbiter in each clock cycle and a mask identifying the relative priority of requests received by the arbiter in the same clock cycle. The operation of the arbiter is verified using an assertion which establishes a relationship between the counter and the clock cycle in which the watched request is output from the arbiter.
Other inventors -
Clock Verification
Issued US 9,563,727
Methods and systems for verifying a derived clock using assertion-based verification. The
method comprises counting the number of full or half cycles of a fast clock that occur between
the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow
clock); counting the number of full or half cycles of the fast clock that occur between the
falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow
clock); and verifying the…Methods and systems for verifying a derived clock using assertion-based verification. The
method comprises counting the number of full or half cycles of a fast clock that occur between
the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow
clock); counting the number of full or half cycles of the fast clock that occur between the
falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow
clock); and verifying the counts using assertion-based verification. -
Hardware data structure for tracking ordered transactions
Issued US 9,519,611
Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design using a counter and an indexed table. In some examples, the
data structure comprises a counter that keeps track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions using the counter; and
control logic that verifies a transaction response has been received in the correct order (e.g.
corresponds to the oldest…Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design using a counter and an indexed table. In some examples, the
data structure comprises a counter that keeps track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions using the counter; and
control logic that verifies a transaction response has been received in the correct order (e.g.
corresponds to the oldest in-flight transaction) based on the age information in the table. -
Hardware data structure for tracking ordered transactions
Issued GB GB2529971
Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design using a counter and an indexed table. In some examples, the
data structure comprises a counter that keeps track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions using the counter; and
control logic that verifies a transaction response has been received in the correct order (e.g.
corresponds to the oldest…Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design using a counter and an indexed table. In some examples, the
data structure comprises a counter that keeps track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions using the counter; and
control logic that verifies a transaction response has been received in the correct order (e.g.
corresponds to the oldest in-flight transaction) based on the age information in the table. -
Hardware data structure for tracking partially ordered and reordered transactions
Issued GB GB2530208
Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design comprising one or more slaves configured to receive
transaction requests from a plurality of masters. In some examples, the data structure
comprises one or more counters for keeping track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions for each master using the
one or more counters; and control logic…Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design comprising one or more slaves configured to receive
transaction requests from a plurality of masters. In some examples, the data structure
comprises one or more counters for keeping track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions for each master using the
one or more counters; and control logic that verifies a transaction response for an in-flight
transaction for a particular master has been issued by the slave in a predetermined order (e.g.
corresponds to the oldest in-flight transaction for that master) based on the tracked age for
the in-flight transaction in the table. -
Arbiter Verification
Issued GB GB2527165
Methods and systems for verifying operation of an arbiter in a hardware design. The arbiter receives a plurality of requests over a plurality of clock cycles, including a monitored request and outputs the requests in priority order. The method includes identifying the requests received by and output from the arbiter in each clock cycle. The priority of the watched request relative to other pending requests in the arbiter is then tracked using a counter that is updated based on the requests…
Methods and systems for verifying operation of an arbiter in a hardware design. The arbiter receives a plurality of requests over a plurality of clock cycles, including a monitored request and outputs the requests in priority order. The method includes identifying the requests received by and output from the arbiter in each clock cycle. The priority of the watched request relative to other pending requests in the arbiter is then tracked using a counter that is updated based on the requests input to and output from the arbiter in each clock cycle and a mask identifying the relative priority of requests received by the arbiter in the same clock cycle. The operation of the arbiter is verified using an assertion which establishes a relationship between the counter and the clock cycle in which the watched request is output from the arbiter.
Other inventors -
Deadlock detection using assertions
Issued GB GB2526052
Methods and systems for detecting deadlock in a hardware design. The method comprises
identifying one or more control signals in the hardware design; generating a state machine for
each of the one or more control signals to track the state of the control signal; generating one
or more assertions for each control signal to detect that the control signal is in a deadlock
state from the state machine; and detecting whether any of the one or more control signal are
in a deadlock…Methods and systems for detecting deadlock in a hardware design. The method comprises
identifying one or more control signals in the hardware design; generating a state machine for
each of the one or more control signals to track the state of the control signal; generating one
or more assertions for each control signal to detect that the control signal is in a deadlock
state from the state machine; and detecting whether any of the one or more control signal are
in a deadlock state using the assertions. The method may also comprise generating one or
more fairness constraints to impose on a particular assertion and detecting the particular
control signal is in the deadlock state using the assertions under the fairness constraints.Other inventors -
Hardware data structure for tracking ordered transactions
Issued GB GB2524128
Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design using a counter and an indexed table. In some examples, the
data structure comprises a counter that keeps track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions using the counter; and
control logic that verifies a transaction response has been received in the correct order (e.g.
corresponds to the oldest…Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design using a counter and an indexed table. In some examples, the
data structure comprises a counter that keeps track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions using the counter; and
control logic that verifies a transaction response has been received in the correct order (e.g.
corresponds to the oldest in-flight transaction) based on the age information in the table. -
Hardware data structure for tracking partially ordered and reordered transactions
Issued GB GB2524344
Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design comprising one or more slaves configured to receive
transaction requests from a plurality of masters. In some examples, the data structure
comprises one or more counters for keeping track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions for each master using the
one or more counters; and control logic…Methods and hardware data structures for tracking ordered transactions in a multi-transactional
hardware design comprising one or more slaves configured to receive
transaction requests from a plurality of masters. In some examples, the data structure
comprises one or more counters for keeping track of the number of in-flight transactions; a
table that keeps track of the age of each of the in-flight transactions for each master using the
one or more counters; and control logic that verifies a transaction response for an in-flight
transaction for a particular master has been issued by the slave in a predetermined order (e.g.
corresponds to the oldest in-flight transaction for that master) based on the tracked age for
the in-flight transaction in the table. -
Clock verification
Issued GB GB2519181
Methods and systems for verifying a derived clock using assertion-based verification. The
method comprises counting the number of full or half cycles of a fast clock that occur between
the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow
clock); counting the number of full or half cycles of the fast clock that occur between the
falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow
clock); and verifying the…Methods and systems for verifying a derived clock using assertion-based verification. The
method comprises counting the number of full or half cycles of a fast clock that occur between
the rising edge and the falling edge of a slow clock (i.e. during the ON phase of the slow
clock); counting the number of full or half cycles of the fast clock that occur between the
falling edge and the rising edge of the slow clock (i.e. during the OFF phase of the slow
clock); and verifying the counts using assertion-based verification. -
Arbiter verification
GB-2546603-B
-
Control path verification of hardware design for pipelined process
GB GB2561299B
Courses
-
System Verilog
-
-
Verilog
-
Honors & Awards
-
Fellow
British Computer Society (BCS)
-
Fellow
The Institution of Electronics and Telecommunication Engineers (IETE)
-
Senior Member
Institute of Electrical and Electronics Engineers (IEEE)
-
Senior Member
Association for Computing Machinery (ACM)
Languages
-
Hindi
Native or bilingual proficiency
-
German
Elementary proficiency
-
English
Native or bilingual proficiency
Organizations
-
University of Southampton
Royal Academy of Engineering Visiting Professor
- Present
Recommendations received
13 people have recommended Ashish
Join now to viewMore activity by Ashish
-
Takaaki Akashi was presented with 3rd place in the 'Best Paper Award' at DVCON 2024 Japan for his presentation 'Introduction of CHERI and how it…
Takaaki Akashi was presented with 3rd place in the 'Best Paper Award' at DVCON 2024 Japan for his presentation 'Introduction of CHERI and how it…
Liked by Ashish Darbari
-
We had an exciting day at DVCon Japan, diving deep into the world of semiconductors and showcasing our expertise in formal verification! Our booth…
We had an exciting day at DVCon Japan, diving deep into the world of semiconductors and showcasing our expertise in formal verification! Our booth…
Liked by Ashish Darbari
-
I had the pleasure of participating in DVCon Japan today, where I had the opportunity to engage in enriching conversations about Formal and…
I had the pleasure of participating in DVCon Japan today, where I had the opportunity to engage in enriching conversations about Formal and…
Liked by Ashish Darbari
-
Congratulations to our new EE Times Editor-in-Chief, Nitin Dahad! 🎉 Dahad brings a wealth of experience and expertise that promises to uphold the…
Congratulations to our new EE Times Editor-in-Chief, Nitin Dahad! 🎉 Dahad brings a wealth of experience and expertise that promises to uphold the…
Liked by Ashish Darbari
-
Congratulations to AMD and Untether AI on submitting their first MLPerf benchmark results! AMD showed its MI300X matches H100's inference…
Congratulations to AMD and Untether AI on submitting their first MLPerf benchmark results! AMD showed its MI300X matches H100's inference…
Liked by Ashish Darbari
-
📢 Attention Tokyo! 🇯🇵 Are you interested in Formal Verification and happen to be in Tokyo on August 29? Join me at DVCon Japan for an insightful…
📢 Attention Tokyo! 🇯🇵 Are you interested in Formal Verification and happen to be in Tokyo on August 29? Join me at DVCon Japan for an insightful…
Liked by Ashish Darbari
-
I have seen this in different groups of different companies. What do you think of these designers who are very sensitive to what to call the design…
I have seen this in different groups of different companies. What do you think of these designers who are very sensitive to what to call the design…
Liked by Ashish Darbari
-
It's a great feeling that 25 PhD students have graduated under my supervision over as many years. This is to thank all of them for working with me…
It's a great feeling that 25 PhD students have graduated under my supervision over as many years. This is to thank all of them for working with me…
Liked by Ashish Darbari
-
Shoutout to Our Amazing Sponsors! We are thrilled to announce and thank our incredible sponsors for their generous support for the upcoming DVCon…
Shoutout to Our Amazing Sponsors! We are thrilled to announce and thank our incredible sponsors for their generous support for the upcoming DVCon…
Liked by Ashish Darbari
-
It is time! Axiomise is excited to be a part of DVCon Japan 2024, where we will showcase our pioneering work in formal verification. Whether you’re…
It is time! Axiomise is excited to be a part of DVCon Japan 2024, where we will showcase our pioneering work in formal verification. Whether you’re…
Liked by Ashish Darbari
-
Super excited to meet up with everyone tomorrow!
Super excited to meet up with everyone tomorrow!
Shared by Ashish Darbari
-
If you had a huge windfall or catastrophic event happen to you, you generally get back to the same level of happiness in time, but there is no…
If you had a huge windfall or catastrophic event happen to you, you generally get back to the same level of happiness in time, but there is no…
Liked by Ashish Darbari
Other similar profiles
Explore collaborative articles
We’re unlocking community knowledge in a new way. Experts add insights directly into each article, started with the help of AI.
Explore MoreOthers named Ashish Darbari
2 others named Ashish Darbari are on LinkedIn
See others named Ashish Darbari