公开(公告)号：DE112018000140T5

公开(公告)日：2019-07-11

申请号：DE112018000140

申请日：2018-01-08

Applicant: IBM

Inventor： KROENER MICHAEL KLAUS ,  KRAUTZ UDO ,  BABINSKY TINA ,  MUELLER SILVIA MELITTA ,  WAGNER ANDREAS

IPC: G06F7/483

Abstract: Gleitkommaeinheit (10), die so konfiguriert ist, dass sie eine verschmolzene Multiplikations-Additions-Operation auf drei 128 Bit breiten Operanden (100, 102, 104) durchführt, wobei die Einheit aufweist: (i) einen 113x113-Bit-Multiplikator (14); (ii) einen Linksverschieber (18); (iii) einen Rechtsverschieber (20); (iv) eine Auswahlschaltung (24), die einen 3-zu-2-Komprimierer (25) aufweist; (v) einen Addierer (26), der mit dem Datenfluss von der Auswahlschaltung (24) verbunden ist; (vi) einen ersten Rückmeldepfad (36), der einen Übertragausgang (91) des Addierers (26) mit der Auswahlschaltung (24) verbindet; und (vii) einen zweiten Rückmeldepfad (38), der den Ausgang des Addierers (26) mit den Verschiebern (18, 20) verbindet, um ein breites Zwischenergebnis (86) über die Verschieber (18, 20) weiterzuleiten.

公开(公告)号：GB2508233A

公开(公告)日：2014-05-28

申请号：GB201221290

申请日：2012-11-27

Applicant: IBM

Inventor： KRAUTZ UDO ,  SCHMIDT ULRIKE ,  BOERSMA MAARTEN

IPC: G06F17/50

Abstract: A logic design for a processor execution unit includes an instruction pipeline 10 with one or more pipeline stages 12 for executing a plurality of instructions. A method of formal verification of the logic design involves selecting an instruction from the plurality of instructions and may verify the processing of that instruction using formal model checking. A design under test is created by using a first 30 and a second 32 instance of the logic design. The first instance 30 is initialized with defined values in each instruction pipeline stage and the second instance 32 with random initial values in each pipeline stage. The instruction is then simultaneously issued to each instance, executed and a comparison of the results output from the instruction pipelines is made 16. If the instruction was verified by formal model checking, approving the correctness of the logic design if the comparison result is true. If the instruction was not verifiable by formal model checking, approving the correctness of a sequenced computation if the comparison result is true.

公开(公告)号：GB2508970B

公开(公告)日：2014-11-26

申请号：GB201318702

申请日：2013-10-23

Applicant: IBM

Inventor： KRAUTZ UDO ,  SCHMIDT ULRIKE ,  BOERSMA MAARTEN

IPC: G06F17/50

公开(公告)号：GB2508970A

公开(公告)日：2014-06-18

申请号：GB201318702

申请日：2013-10-23

Applicant: IBM

Inventor： KRAUTZ UDO ,  SCHMIDT ULRIKE ,  BOERSMA MAARTEN

IPC: G06F17/50

Abstract: A logic design for a processor execution unit includes an instruction pipeline 10 with one or more pipeline stages 12 for executing a plurality of instructions. A method of formal verification of the logic design involves selecting an instruction from the plurality of instructions and may verify the processing of that instruction using formal model checking. A design under test is created by using a first 30 and a second 32 instance of the logic design. The first instance 30 is initialized with defined values in each instruction pipeline stage and the second instance 32 with random initial values in each pipeline stage. The instruction is then simultaneously issued to each instance, executed and a comparison of the results output from the instruction pipelines is made 16. If the instruction was verified by formal model checking, approving the correctness of the logic design if the comparison result is true. If the instruction was not verifiable by formal model checking, approving the correctness of a sequenced computation if the comparison result is true.