Max Depth:

Bug 80 depends on 42 bugs:

view as bug list

•    80: Formal Mathematical Proofs needed [CONFIRMED; assigned to lkcl]
  •    61: Evaluate and research Formal Mathematical Proofs [CONFIRMED; assigned to lkcl]
  •    158: NLNet 2019 Formal Correctness Proofs toplevel 2019-10-032 [RESOLVED FIXED; assigned to 2019-10P]
    •    211: formal proof of PowerDecoder stage2 needed [CONFIRMED; assigned to lkcl]
    •    195: Formal correctness framework is needed for Power ISA [RESOLVED FIXED; assigned to lkcl]
      •    211: formal proof of PowerDecoder stage2 needed [CONFIRMED; assigned to lkcl] (*)
      •    306: Formal Correctness Proof for ALU pipeline [RESOLVED FIXED; assigned to kc5tja]
        •    429: pipeline main_stage formal verification does not check ctx fields fully [CONFIRMED; assigned to kc5tja]
        •    337: Convention for register outputs in *OutputData structures is to use "Data" [RESOLVED FIXED; assigned to lkcl]
      •    331: Formal Correctness Proof for LOGICAL pipeline [RESOLVED FIXED; assigned to lkcl]
      •    332: Formal correctness proof needed for CR pipeline [RESOLVED FIXED; assigned to mtnolan2640]
      •    418: SPR pipeline formal correctness proof needed [RESOLVED FIXED; assigned to kc5tja]
        •    429: pipeline main_stage formal verification does not check ctx fields fully [CONFIRMED; assigned to kc5tja] (*)
      •    419: MUL pipeline formal proof needed [RESOLVED FIXED; assigned to kc5tja]
        •    482: mul ok and ov must not be unconditionally set [RESOLVED FIXED; assigned to lkcl]
    •    196: Formal correctness proof needed for the IEEE754 FPU [RESOLVED FIXED; assigned to lkcl]
      •    596: formal correctness proof for nmigen integration of Dynamic Partitioned Signal [CONFIRMED; assigned to mail]
      •    868: Formal verification of fadd/fsub [IN_PROGRESS; assigned to programmerjake]
        •    835: add support for smtlib2 floating-point to yosys and nmigen [RESOLVED FIXED; assigned to programmerjake]
        •    869: Formal verification of fadd for just round-nearest-ties-to-even without exception flags/traps [RESOLVED FIXED; assigned to programmerjake]
          •    835: add support for smtlib2 floating-point to yosys and nmigen [RESOLVED FIXED; assigned to programmerjake] (*)
        •    874: Implementation and Formal verification of fadd for all rounding modes but without exception flags/traps [RESOLVED FIXED; assigned to programmerjake]
          •    835: add support for smtlib2 floating-point to yosys and nmigen [RESOLVED FIXED; assigned to programmerjake] (*)
        •    876: Implement and Add Formal Proof for fsub in the fpadd pipeline [RESOLVED FIXED; assigned to programmerjake]
          •    835: add support for smtlib2 floating-point to yosys and nmigen [RESOLVED FIXED; assigned to programmerjake] (*)
      •    162: Formally Verify the FSGNJ module [PAYMENTPENDING FIXED; assigned to mtnolan2640]
      •    163: Formally Verify the FPMAX module [PAYMENTPENDING FIXED; assigned to mtnolan2640]
      •    165: Formally verify the FPCMP (FEQ, FLE, FLT) module [PAYMENTPENDING FIXED; assigned to mtnolan2640]
      •    835: add support for smtlib2 floating-point to yosys and nmigen [RESOLVED FIXED; assigned to programmerjake] (*)
      •    877: implementation and formal correctness proof for fp fused-mul-add pipeline excluding ieee754 exception flags [RESOLVED FIXED; assigned to programmerjake]
        •    835: add support for smtlib2 floating-point to yosys and nmigen [RESOLVED FIXED; assigned to programmerjake] (*)
    •    197: Formal correctness proof needed of the 6600-style Out-of-Order execution engine [RESOLVED FIXED; assigned to lkcl]
      •    879: Formal proof of soc.experiment.compalu_multi.MultiCompUnit needed [RESOLVED FIXED; assigned to cestrauss]
    •    198: Formal correctness proofs are needed for low-level libraries in LibreSOC [RESOLVED FIXED; assigned to programmerjake]
      •    211: formal proof of PowerDecoder stage2 needed [CONFIRMED; assigned to lkcl] (*)
      •    901: Formal proof for PriorityPicker and MultiPriorityPicker and BetterMultiPriorityPicker [RESOLVED FIXED; assigned to programmerjake]
      •    902: Formal proof for nmutil byterev.py [RESOLVED FIXED; assigned to programmerjake]
      •    903: Formal proof for nmigen.queue.Queue [RESOLVED FIXED; assigned to programmerjake]
      •    904: Formal proof for pop-count [RESOLVED FIXED; assigned to programmerjake]
      •    909: Formal proof of nmutil/plru.py [RESOLVED FIXED; assigned to programmerjake]
    •    577: gcc compiler, binutils and assembly macros for OpenPOWER-SV [RESOLVED FIXED; assigned to lkcl]
      •    579: c/c++ macros for inline assembly supporting svp64 [IN_PROGRESS; assigned to programmerjake]
      •    836: binutils: support the rest of bitmanip instructions [CONFIRMED; assigned to ghostmansd]
        •    852: implement grevlut* [CONFIRMED; assigned to lkcl]
      •    550: binutils support needed for svp64 [RESOLVED FIXED; assigned to lkcl]
        •    867: add svindex instruction to binutils (and openpower-isa infrastructure) [RESOLVED FIXED; assigned to ghostmansd]
        •    872: binutil needs support for new Pack/Unpack modes [RESOLVED INVALID; assigned to ghostmansd]
          •    871: implement pack/unpack mode in ISACaller [RESOLVED FIXED; assigned to lkcl]
      •    578: python-based svp64 "generator" class [RESOLVED FIXED; assigned to lkcl]
      •    834: binutils: support draft fsins/fcoss/ternlogi instructions [RESOLVED FIXED; assigned to ghostmansd]
      •    907: structure packing SVG [RESOLVED FIXED; assigned to veerakumar.r]

Bug 80 blocks one bug:

view as bug list

•    80: Formal Mathematical Proofs needed [CONFIRMED; assigned to lkcl]
  •    487: Canonical Root bug for budgeting purposes for the "Future" milestone [DEFERRED; assigned to lkcl]

Max Depth:

• • Home
  • | New
  • | Browse
  • | Search
  • |
    [?]
  • | Reports
  • | Help
  • | Log In
    [x]
  • | Forgot Password
    Login: [x]