公开(公告)号：US11501050B1

公开(公告)日：2022-11-15

申请号：US17176993

申请日：2021-02-16

Applicant: Synopsys, Inc.

Inventor： Dmitry Korchemny ,  Eduard R. Cerny ,  Ilya Kudryavtsev

IPC: G06F119/02 ,  G06F30/367 ,  G06F30/38

Abstract: A design for an analog mixed-signal (AMS) circuit is accessed. An assertion for verifying the behavior of an analog signal in the AMS circuit is also accessed. The assertion is expressed in an assertion language for AMS circuits. A processor verifies the assertion against the predicted behavior of the analog signal in the AMS circuit. In various embodiments, the assertion language contains predefined classes for assertions in the temporal domain, for assertions in the frequency domain, and for assertions based on functional dependencies of an output analog signal on an input analog signal.

公开(公告)号：US20240273271A1

公开(公告)日：2024-08-15

申请号：US18167861

申请日：2023-02-12

Applicant: Synopsys, Inc.

Inventor： Dmitry Korchemny ,  Naphtali Yehoshua Sprei ,  Ilya Kudryavtsev

IPC: G06F30/33 ,  G06F30/327

CPC classification number: G06F30/33 ,  G06F30/327 ,  G06F2119/02

Abstract: An assertion for a sequential implication for a circuit design is received. The sequential implication defines a nonoverlapping transaction in which new transactions are not allowed while an existing transaction is still pending. The assertion is converted to a deterministic finite automaton on finite words in a machine-readable form, which is made available to verify the operation of the circuit design.

公开(公告)号：US20200034499A1

公开(公告)日：2020-01-30

申请号：US16173933

申请日：2018-10-29

Applicant: Synopsys, Inc.

Inventor： Ionut Silviu Cirjan ,  Boris Gommershtadt ,  Dmitry Korchemny ,  Naphtali Yehoshua Sprei

IPC: G06F17/50

Abstract: Forming a logic circuit design from a behavioral description language that includes N force and M release statements applied to a net disposed in the design, includes, in part, forming N multiplexers and a controller controlling the select terminals of the N multiplexers. Each multiplexer receives a force signal at its first input terminal. The output signal of the ith multiplexer is supplied to a second input terminal of (i+1)th multiplexer. A driver signal driving the net in the absence of the force statements is applied to a second input terminal of a first multiplexer. The controller asserts the select signal of the ith multiplexer if the ith force condition is active, and unasserts the select signal of the ith multiplexer if any one of a number of predefined conditions is satisfied.

公开(公告)号：US20230214574A1

公开(公告)日：2023-07-06

申请号：US18068371

申请日：2022-12-19

Applicant: Synopsys, Inc.

Inventor： Dmitry Korchemny

IPC: G06F30/398 ,  G06F30/392

CPC classification number: G06F30/398 ,  G06F30/392

Abstract: A directed acyclic graph (DAG) and an extended regular expression (ERE) may be received. A circuit design may be generated based on the DAG. A cover property may be generated based on the ERE. The circuit design may be simulated. A first result may be determined based on whether the cover property is satisfied during the simulating the circuit design. It may be determined whether the ERE matches a path in the DAG based on the first result.

公开(公告)号：US10962595B1

公开(公告)日：2021-03-30

申请号：US16192660

申请日：2018-11-15

Applicant: Synopsys, Inc.

Inventor： Leonid Alexander Broukhis ,  Boris Gommershtadt ,  Florent Duru ,  Gabriel Gouvine ,  Dmitry Korchemny

IPC: G01R31/3185 ,  G06F11/26 ,  G06F9/30 ,  G06F11/267 ,  G06F30/331 ,  G01R31/327

Abstract: Coverage event counters for hardware verification emulations are implemented as linear feedback shift register-based counters generating encoded counter values indicative of a detected number of coverage events. To decode those counter values, a counter algorithm utilized to generate the encoded counter value may continue to be iterated after counting is complete until reaching a defined pattern, while counting the number of iterations (K) necessary to reach the defined pattern. The resulting counter value having the defined pattern is correlated with a mapping table to identify a numerical value, and an ordinal counter value indicative of the number of coverage events is determined based on the identified numerical value, less K.

公开(公告)号：US10579760B2

公开(公告)日：2020-03-03

申请号：US16173933

申请日：2018-10-29

Applicant: Synopsys, Inc.

Inventor： Ionut Silviu Cirjan ,  Boris Gommershtadt ,  Dmitry Korchemny ,  Naphtali Yehoshua Sprei

IPC: G06F17/50

Abstract: Forming a logic circuit design from a behavioral description language that includes N force and M release statements applied to a net disposed in the design, includes, in part, forming N multiplexers and a controller controlling the select terminals of the N multiplexers. Each multiplexer receives a force signal at its first input terminal. The output signal of the ith multiplexer is supplied to a second input terminal of (i+1)th multiplexer. A driver signal driving the net in the absence of the force statements is applied to a second input terminal of a first multiplexer. The controller asserts the select signal of the ith multiplexer if the ith force condition is active, and unasserts the select signal of the ith multiplexer if any one of a number of predefined conditions is satisfied.

公开(公告)号：US20230017872A1

公开(公告)日：2023-01-19

申请号：US17859649

申请日：2022-07-07

Applicant: Synopsys, Inc.

Inventor： Dmitry Korchemny ,  Naphtali Yehoshua Sprei

IPC: G06F30/398

Abstract: A system receives assertions representing properties of a circuit design. The system determines a representation of an alternating Büchi automaton based on the assertions. The system transforms the representation of the alternating Büchi automaton to generate a representation of a simplified alternating Büchi automaton. The simplified alternating Büchi automaton has fewer states than the alternating Büchi automaton. One or more states of the simplified alternating Büchi automaton are obtained by merging states of the alternating Büchi automaton representing the assertions of the circuit. The system performs formal verification of the circuit design using the simplified alternating Büchi automaton.

公开(公告)号：US11188695B2

公开(公告)日：2021-11-30

申请号：US16058157

申请日：2018-08-08

Applicant: Synopsys, Inc.

Inventor： Dmitry Korchemny ,  Ashok Kumar Bhatt ,  Eduard Rudolf Cerny ,  Hanish Singla

IPC: G06F30/30 ,  G06F30/331 ,  G06F30/3323

Abstract: Synthesis of functional coverage (e.g., covergroups) is optimized for hardware emulation. The optimization may reduce the number of logic gates used to implement the hardware emulator circuits or reduce the computer resources used to synthesize the hardware emulator circuits. The optimization may also prevent the synthesis of unnecessary circuits. In another aspect, the optimization may result in a representation that may be used both to synthesize hardware emulation circuits and as part of formal verification. This may result in a model that can be used for formal verification, hardware emulation, and software simulation.

公开(公告)号：US20190050516A1

公开(公告)日：2019-02-14

申请号：US16058157

申请日：2018-08-08

Applicant: Synopsys, Inc.

Inventor： Dmitry Korchemny ,  Ashok Kumar Bhatt ,  Eduard Rudolf Cerny ,  Hanish Singla

IPC: G06F17/50

Abstract: Synthesis of functional coverage (e.g., covergroups) is optimized for hardware emulation. The optimization may reduce the number of logic gates used to implement the hardware emulator circuits or reduce the computer resources used to synthesize the hardware emulator circuits. The optimization may also prevent the synthesis of unnecessary circuits. In another aspect, the optimization may result in a representation that may be used both to synthesize hardware emulation circuits and as part of formal verification. This may result in a model that can be used for formal verification, hardware emulation, and software simulation.

公开(公告)号：US11544435B1

公开(公告)日：2023-01-03

申请号：US17353208

申请日：2021-06-21

Applicant: Synopsys, Inc.

Inventor： Dmitry Korchemny ,  Ilya Kudryavtsev ,  Eduard Cerny ,  Dmitriy Mosheyev

IPC: G06F30/3308 ,  G06F30/38 ,  G06F30/327 ,  G06F30/367 ,  G06F30/398

Abstract: The present disclosure generally relates to an analog mixed-signal (AMS) design verification system. In particular, the present disclosure relates to a system and method for system verification. One example method includes: obtaining an electronic representation of the circuit design; generating at least a portion of a waveform using the electronic representation of the circuit to obtain a first segment of the waveform associated with the circuit; converting, via the one or more processors, one or more measurement functions to code for performing the one or more computations on the first segment of the waveform; performing one or more computations on the first segment of the waveform using the code; and identifying when a behavior of the circuit violates a design specification based on whether a result of the one or more computations meets a threshold.