Amazon Technologies, Inc.

Uri Leder

Benzi Denkberg

Guy Nakibly

Nafea Bshara

Erez Izenberg

Ofer Frishman

Max Chvalevsky

Adi Habusha

Ori Ariel

Ori Weber

Ofer Naaman

Itai Avron

Tzachi Zidenberg

Ori Cohen

Roi Ben Haim

Sergey Kleyman

Svetlana Kantorovych

Ohad Gdalyahu

Simaan Bahouth

Assaf Fainer

Ariel Pescovsky

Muhamad Grefat

Itai Kahana

Hani Assaf

Yefim Fainstein

Cover properties are extended in formal verification to reach an effective end-of-test stage for a design under test. A formal verification task for a design under test may be received at a verification system. A cover property asserted in the formal verification task may be identified. An additional condition may be implemented for the identified cover property to extend the identified cover property to cause performance of the formal verification task to generate a trace to reach an effective end-of-test stage for the design under test in the event of a failure of the cover property.

Extending cover properties in formal verification to generate failure traces that reach end-of-test

A link layer reliability (LLR) circuit of a communication device can receive an indication that a link down event has occurred on a bus link with a peer device. The LLR circuit can prevent the link down event from triggering a reset of configuration registers containing bus settings for the bus link. Once the bus link has been restored, the LLR circuit can send a retry request to the peer device indicating an expected sequence number associated with a transaction that the LLR circuit is expecting from the peer device. The LLR circuit may receive a retry acknowledgment from the peer device indicating receipt of the retry request for the transaction corresponding to the expected sequence number, and payload data for the transaction corresponding to the expected sequence number.

Link down resilience

Generated instruction sequences captured from software interactions may be executed as part of formal verification of a design under test. Software-instructed commands to be performed to configure a design under test formatted according to an interface implemented by the design under test can be obtained. A sequence to perform the software-instructed commands may be generated to configure the design under test in a hardware design and verification language. The sequence may then be executed to perform the software-instructed commands to configure the design under test and then perform formal verification on the configured design under test.

Executing instruction sequences generated from software interactions as part of formal verification of a design under test

A fuzzy scoreboard can compute, using a signature function, a first signature of an expected data stream associated with an input data stream that is being inputted to a design-under-test (DUT) for a datapath test. The first signature of the expected data stream can be stored without storing the expected data stream. The fuzzy scoreboard can also compute, using the same signature function, a second signature of an output data stream that is outputted from the DUT during the datapath test. The first signature can be compared with the second signature to determine whether there is a match. Storing the first signature of the expected data stream without storing the expected data stream can reduce the memory space consumed by the fuzzy scoreboard.

Fuzzy scoreboard

An integrated circuit design technique utilizes a data structure describing the connections, interconnect routing information of the connections, and bandwidth requirements of the connections in an integrated circuit device to generate an interconnect flow graph having nodes, and edges connecting the nodes. The edges connecting the nodes can reflect the bandwidth requirements of the connections. The interconnect flow graph can be used to optimize and verify the integrated circuit design.

Interconnect flow graph for integrated circuit design

Hardware-software interaction testing is performed using formal verification for language-specified hardware designs. A description of valid access using an interface for a configuration space of a language specified hardware design and a description of a valid output of the language-specified hardware design is received. Formal verification is performed on the language-specified hardware design using the interface for the configuration space according to the description of valid access using the interface. A sequence of access to the configuration space using the interface that causes a failure to produce the valid output of the language-specified hardware design according to the description of valid output to identify as an error for the language-specified hardware design.

Hardware-software interaction testing using formal verification

A dedicated input/output (I/O) cache can be used for I/O-to-processor communications. Data received from an I/O device can be written to the I/O cache and also written to a device memory that is accessible to the processor. The processor can then access the data in the fast, dedicated I/O cache if available. Otherwise, the processor can read the data from the memory into a conventional processor cache for processing. Writes to the cache can be full or partial, with partial writes utilizing padding in some embodiments. The data can be written sequentially in a circular manner. Data processed by the processor can be invalidated, and invalidated data can be overwritten on a subsequent write. Phase bits can also be used to indicate the pass during which various writes were performed.

Dedicated communications cache

Environmental modification testing with a formal verification is implemented for language-specified hardware designs. A language-specified hardware design may be received. A reference copy of the language-specified hardware design may be created. A formal verification may be performed on both the language-specified hardware design and the reference copy with a same input data. Different environmental assumptions for processing the same input data through the reference copy and the language-specified hardware design may be applied. An output value of the language-specified hardware design may be compared with an output value of the reference copy to determine whether those output values match. Error indications may be provided based on a result of the comparison.

Environmental modification testing for design correctness with formal verification

A data or packet processing device such as a network interface controller may include cache control logic that is configured to obtain a set of memory descriptors associated with a queue from the memory. The set of descriptors can be stored in the cache. When a request for processing a data packet associated with the queue is received, the cache control logic can determine that the cache is storing memory descriptors for processing the data packet, and provide the memory descriptors used for processing the packet.

Packet processing cache

Interactive compilation of software to a hardware language may be performed to satisfy formal verification constraints. Source code for software to be executed on a hardware design may be received. Intermediate code may be generated from the source code as part of translating the source code to a hardware language used to specify the hardware design. The intermediate code may be provided via an interface and updates to the intermediate code may be received. The updated source code may then be used to complete translation of the source code to the hardware language.

Interactive compilation of software to a hardware language to satisfy formal verification constraints

A data or packet processing device such as a network interface controller may include cache control logic that is configured to receive a first request for processing a first data packet associated with the queue identifier, and obtain a set of memory descriptors associated with the queue identifier from the memory. The set of descriptors can be stored in the cache. When a second request for processing a second data packet associated with the queue identifier is received, the cache control logic can determine that the cache is storing memory descriptors for processing the second data packet, and provide the memory descriptors used for processing the second packet.

Techniques for controlling access to shared resources may include receiving multiple requests to access shared information associated with an identifier. For each of the requests, an entry in a linked list can be allocated to the request, and each entry can be associated with the identifier. The shared information associated with the identifier can be retrieved, and stored in each entry associated with the identifier. A conflict indicator is set in each entry to indicate whether the shared information is available for the request corresponding to the entry. The shared information stored in each entry is provided for each request after the conflict indicator in the corresponding entry indicates the shared information is available for the request.

Growing community of inventors

Lotem, Israel

Uri Leder