default attribute of 
  indexA (rs1, rs2) is 
    (/\#n where #32 divides #n. 
      <RTLOP add> #n 
        (FETCH_METHOD #n (AGG_METHOD #32 #n ($r rs1))
        , FETCH_METHOD #n (AGG_METHOD #32 #n ($r rs2))
        )) : (\/ #n where #32 divides #n . #n bits)

default attribute of 
  dispA (rs1, simm13) is 
    (/\#n where #32 divides #n. 
      <RTLOP add> #n 
        (FETCH_METHOD #n (AGG_METHOD #32 #n ($r rs1))
        , <RTLOP sx> #13 #n simm13
        )) : (\/ #n where #32 divides #n . #n bits)

default attribute of rmode rs2 is $r rs2 : #32 cell

default attribute of 
  imode simm13 is (/\#n. <RTLOP sx> #13 #n simm13) : (\/ #n . #n bits)

default attribute of 
  ldsb (address, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP sx> #8 #32 (FETCH_METHOD #8 (AGG_METHOD #8 #8 ($m address)))
      ) : rtl

default attribute of 
  ldsh (address, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP sx> #32 #32 (FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address)))
      ) : rtl

default attribute of 
  ldub (address, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP zx> #8 #32 (FETCH_METHOD #8 (AGG_METHOD #8 #8 ($m address)))
      ) : rtl

default attribute of 
  lduh (address, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP zx> #32 #32 (FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address)))
      ) : rtl

default attribute of 
  ld (address, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address))
      ) : rtl

default attribute of 
  ldd (address, rd) is 
    STORE_METHOD #64 
      (AGG_METHOD #32 #64 ($r rd)
      , FETCH_METHOD #64 (AGG_METHOD #8 #64 ($m address))
      ) : rtl

default attribute of 
  sth (rd, address) is 
    STORE_METHOD #16 
      (AGG_METHOD #8 #16 ($m address)
      , 16-bits-at #ungeneralized-26 #32 
        (0 #ungeneralized-26, FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rd)))
      ) : rtl

default attribute of 
  stb (rd, address) is 
    STORE_METHOD #8 
      (AGG_METHOD #8 #8 ($m address)
      , 8-bits-at #ungeneralized-27 #32 
        (0 #ungeneralized-27, FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rd)))
      ) : rtl

default attribute of 
  st (rd, address) is 
    STORE_METHOD #32 
      (AGG_METHOD #8 #32 ($m address)
      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rd))
      ) : rtl

default attribute of 
  std (rd, address) is 
    STORE_METHOD #64 
      (AGG_METHOD #8 #64 ($m address)
      , FETCH_METHOD #64 (AGG_METHOD #32 #64 ($r rd))
      ) : rtl

default attribute of 
  ldstub (address, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP zx> #8 #32 (FETCH_METHOD #8 (AGG_METHOD #8 #8 ($m address)))
        )
      , STORE_METHOD #8 (AGG_METHOD #8 #8 ($m address), 255 #8)
      ) : rtl

default attribute of 
  swap (address, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address))
        )
      , STORE_METHOD #32 
        (AGG_METHOD #8 #32 ($m address)
        , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rd))
        )
      ) : rtl

default attribute of 
  save (rs1, reg_or_imm, rd) is 
    ; 
      (; 
        (; 
          (; 
            (; 
              (--> 
                (<RTLOP ne> #5 (rd, <RTLOP add> #5 (0, 24 #5))
                , STORE_METHOD #32 
                  (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 24 #5)))
                  , FETCH_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 8 #5))))
                  )
                )
              , ; 
                (--> 
                  (<RTLOP ne> #5 (rd, <RTLOP add> #5 (1, 24 #5))
                  , STORE_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 24 #5)))
                    , FETCH_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 8 #5))))
                    )
                  )
                , ; 
                  (--> 
                    (<RTLOP ne> #5 (rd, <RTLOP add> #5 (2, 24 #5))
                    , STORE_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 24 #5)))
                      , FETCH_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 8 #5))))
                      )
                    )
                  , ; 
                    (--> 
                      (<RTLOP ne> #5 (rd, <RTLOP add> #5 (3, 24 #5))
                      , STORE_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (3, 24 #5)))
                        , FETCH_METHOD #32 
                          (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (3, 8 #5))))
                        )
                      )
                    , ; 
                      (--> 
                        (<RTLOP ne> #5 (rd, <RTLOP add> #5 (4, 24 #5))
                        , STORE_METHOD #32 
                          (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (4, 24 #5)))
                          , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (4, 8 #5))))
                          )
                        )
                      , ; 
                        (--> 
                          (<RTLOP ne> #5 (rd, <RTLOP add> #5 (5, 24 #5))
                          , STORE_METHOD #32 
                            (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (5, 24 #5)))
                            , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (5, 8 #5))))
                            )
                          )
                        , ; 
                          (--> 
                            (<RTLOP ne> #5 (rd, <RTLOP add> #5 (6, 24 #5))
                            , STORE_METHOD #32 
                              (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (6, 24 #5)))
                              , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                  ($r (<RTLOP add> #5 (6, 8 #5))))
                              )
                            )
                          , ; 
                            (--> 
                              (<RTLOP ne> #5 (rd, <RTLOP add> #5 (7, 24 #5))
                              , STORE_METHOD #32 
                                (AGG_METHOD #32 #32 
                                  ($r (<RTLOP add> #5 (7, 24 #5)))
                                , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                    ($r (<RTLOP add> #5 (7, 8 #5))))
                                )
                              )
                            , SKIP
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            , ; 
              (STORE_METHOD #32 
                (AGG-ID #32 ($w (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 8 #32)
                      , <RTLOP zx> #5 #32 0
                      )))
                , FETCH_METHOD #32 
                  (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 16 #5))))
                )
              , ; 
                (STORE_METHOD #32 
                  (AGG-ID #32 ($w (<RTLOP add> #32 
                        (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 8 #32)
                        , <RTLOP zx> #5 #32 1
                        )))
                  , FETCH_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 16 #5))))
                  )
                , ; 
                  (STORE_METHOD #32 
                    (AGG-ID #32 ($w (<RTLOP add> #32 
                          (<RTLOP add> #32 
                            (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 8 #32)
                          , <RTLOP zx> #5 #32 2
                          )))
                    , FETCH_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 16 #5))))
                    )
                  , ; 
                    (STORE_METHOD #32 
                      (AGG-ID #32 ($w (<RTLOP add> #32 
                            (<RTLOP add> #32 
                              (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                              , 8 #32
                              )
                            , <RTLOP zx> #5 #32 3
                            )))
                      , FETCH_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (3, 16 #5))))
                      )
                    , ; 
                      (STORE_METHOD #32 
                        (AGG-ID #32 ($w (<RTLOP add> #32 
                              (<RTLOP add> #32 
                                (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                , 8 #32
                                )
                              , <RTLOP zx> #5 #32 4
                              )))
                        , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                            ($r (<RTLOP add> #5 (4, 16 #5))))
                        )
                      , ; 
                        (STORE_METHOD #32 
                          (AGG-ID #32 ($w (<RTLOP add> #32 
                                (<RTLOP add> #32 
                                  (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                  , 8 #32
                                  )
                                , <RTLOP zx> #5 #32 5
                                )))
                          , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (5, 16 #5))))
                          )
                        , ; 
                          (STORE_METHOD #32 
                            (AGG-ID #32 ($w (<RTLOP add> #32 
                                  (<RTLOP add> #32 
                                    (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                    , 8 #32
                                    )
                                  , <RTLOP zx> #5 #32 6
                                  )))
                            , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (6, 16 #5))))
                            )
                          , ; 
                            (STORE_METHOD #32 
                              (AGG-ID #32 ($w (<RTLOP add> #32 
                                    (<RTLOP add> #32 
                                      (FETCH_METHOD #32 
                                        (AGG-ID #32 ($W (0 #1)))
                                      , 8 #32
                                      )
                                    , <RTLOP zx> #5 #32 7
                                    )))
                              , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                  ($r (<RTLOP add> #5 (7, 16 #5))))
                              )
                            , SKIP
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          , ; 
            (STORE_METHOD #32 
              (AGG-ID #32 ($w (<RTLOP add> #32 
                    (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                    , <RTLOP zx> #5 #32 0
                    )))
              , FETCH_METHOD #32 
                (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 24 #5))))
              )
            , ; 
              (STORE_METHOD #32 
                (AGG-ID #32 ($w (<RTLOP add> #32 
                      (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                      , <RTLOP zx> #5 #32 1
                      )))
                , FETCH_METHOD #32 
                  (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 24 #5))))
                )
              , ; 
                (STORE_METHOD #32 
                  (AGG-ID #32 ($w (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                        , <RTLOP zx> #5 #32 2
                        )))
                  , FETCH_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 24 #5))))
                  )
                , ; 
                  (STORE_METHOD #32 
                    (AGG-ID #32 ($w (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                          , <RTLOP zx> #5 #32 3
                          )))
                    , FETCH_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (3, 24 #5))))
                    )
                  , ; 
                    (STORE_METHOD #32 
                      (AGG-ID #32 ($w (<RTLOP add> #32 
                            (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                            , <RTLOP zx> #5 #32 4
                            )))
                      , FETCH_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (4, 24 #5))))
                      )
                    , ; 
                      (STORE_METHOD #32 
                        (AGG-ID #32 ($w (<RTLOP add> #32 
                              (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                              , <RTLOP zx> #5 #32 5
                              )))
                        , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                            ($r (<RTLOP add> #5 (5, 24 #5))))
                        )
                      , ; 
                        (STORE_METHOD #32 
                          (AGG-ID #32 ($w (<RTLOP add> #32 
                                (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                , <RTLOP zx> #5 #32 6
                                )))
                          , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (6, 24 #5))))
                          )
                        , ; 
                          (STORE_METHOD #32 
                            (AGG-ID #32 ($w (<RTLOP add> #32 
                                  (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                  , <RTLOP zx> #5 #32 7
                                  )))
                            , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (7, 24 #5))))
                            )
                          , SKIP
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        , STORE_METHOD #32 
          (AGG-ID #32 ($W (0 #1))
          , <RTLOP add> #32 
            (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 16 #32)
          )
        )
      , STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      ) : rtl

default attribute of 
  restore (rs1, reg_or_imm, rd) is 
    ; 
      (; 
        (; 
          (; 
            (; 
              (--> 
                (<RTLOP ne> #5 (rd, <RTLOP add> #5 (0, 8 #5))
                , STORE_METHOD #32 
                  (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 8 #5)))
                  , FETCH_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 24 #5))))
                  )
                )
              , ; 
                (--> 
                  (<RTLOP ne> #5 (rd, <RTLOP add> #5 (1, 8 #5))
                  , STORE_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 8 #5)))
                    , FETCH_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 24 #5))))
                    )
                  )
                , ; 
                  (--> 
                    (<RTLOP ne> #5 (rd, <RTLOP add> #5 (2, 8 #5))
                    , STORE_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 8 #5)))
                      , FETCH_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 24 #5))))
                      )
                    )
                  , ; 
                    (--> 
                      (<RTLOP ne> #5 (rd, <RTLOP add> #5 (3, 8 #5))
                      , STORE_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (3, 8 #5)))
                        , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                            ($r (<RTLOP add> #5 (3, 24 #5))))
                        )
                      )
                    , ; 
                      (--> 
                        (<RTLOP ne> #5 (rd, <RTLOP add> #5 (4, 8 #5))
                        , STORE_METHOD #32 
                          (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (4, 8 #5)))
                          , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (4, 24 #5))))
                          )
                        )
                      , ; 
                        (--> 
                          (<RTLOP ne> #5 (rd, <RTLOP add> #5 (5, 8 #5))
                          , STORE_METHOD #32 
                            (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (5, 8 #5)))
                            , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (5, 24 #5))))
                            )
                          )
                        , ; 
                          (--> 
                            (<RTLOP ne> #5 (rd, <RTLOP add> #5 (6, 8 #5))
                            , STORE_METHOD #32 
                              (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (6, 8 #5)))
                              , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                  ($r (<RTLOP add> #5 (6, 24 #5))))
                              )
                            )
                          , ; 
                            (--> 
                              (<RTLOP ne> #5 (rd, <RTLOP add> #5 (7, 8 #5))
                              , STORE_METHOD #32 
                                (AGG_METHOD #32 #32 
                                  ($r (<RTLOP add> #5 (7, 8 #5)))
                                , FETCH_METHOD #32 (AGG_METHOD #32 #32 
                                    ($r (<RTLOP add> #5 (7, 24 #5))))
                                )
                              )
                            , SKIP
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            , ; 
              (--> 
                (<RTLOP ne> #5 (rd, <RTLOP add> #5 (0, 16 #5))
                , STORE_METHOD #32 
                  (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 16 #5)))
                  , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                          (<RTLOP sub> #32 
                            (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 8 #32)
                          , <RTLOP zx> #5 #32 0
                          ))))
                  )
                )
              , ; 
                (--> 
                  (<RTLOP ne> #5 (rd, <RTLOP add> #5 (1, 16 #5))
                  , STORE_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 16 #5)))
                    , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                            (<RTLOP sub> #32 
                              (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                              , 8 #32
                              )
                            , <RTLOP zx> #5 #32 1
                            ))))
                    )
                  )
                , ; 
                  (--> 
                    (<RTLOP ne> #5 (rd, <RTLOP add> #5 (2, 16 #5))
                    , STORE_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 16 #5)))
                      , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                              (<RTLOP sub> #32 
                                (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                , 8 #32
                                )
                              , <RTLOP zx> #5 #32 2
                              ))))
                      )
                    )
                  , ; 
                    (--> 
                      (<RTLOP ne> #5 (rd, <RTLOP add> #5 (3, 16 #5))
                      , STORE_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (3, 16 #5)))
                        , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                                (<RTLOP sub> #32 
                                  (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                  , 8 #32
                                  )
                                , <RTLOP zx> #5 #32 3
                                ))))
                        )
                      )
                    , ; 
                      (--> 
                        (<RTLOP ne> #5 (rd, <RTLOP add> #5 (4, 16 #5))
                        , STORE_METHOD #32 
                          (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (4, 16 #5)))
                          , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                                  (<RTLOP sub> #32 
                                    (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                    , 8 #32
                                    )
                                  , <RTLOP zx> #5 #32 4
                                  ))))
                          )
                        )
                      , ; 
                        (--> 
                          (<RTLOP ne> #5 (rd, <RTLOP add> #5 (5, 16 #5))
                          , STORE_METHOD #32 
                            (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (5, 16 #5)))
                            , FETCH_METHOD #32 
                              (AGG-ID #32 ($w (<RTLOP add> #32 
                                    (<RTLOP sub> #32 
                                      (FETCH_METHOD #32 
                                        (AGG-ID #32 ($W (0 #1)))
                                      , 8 #32
                                      )
                                    , <RTLOP zx> #5 #32 5
                                    ))))
                            )
                          )
                        , ; 
                          (--> 
                            (<RTLOP ne> #5 (rd, <RTLOP add> #5 (6, 16 #5))
                            , STORE_METHOD #32 
                              (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (6, 16 #5)))
                              , FETCH_METHOD #32 
                                (AGG-ID #32 ($w (<RTLOP add> #32 
                                      (<RTLOP sub> #32 
                                        (FETCH_METHOD #32 
                                          (AGG-ID #32 ($W (0 #1)))
                                        , 8 #32
                                        )
                                      , <RTLOP zx> #5 #32 6
                                      ))))
                              )
                            )
                          , ; 
                            (--> 
                              (<RTLOP ne> #5 (rd, <RTLOP add> #5 (7, 16 #5))
                              , STORE_METHOD #32 
                                (AGG_METHOD #32 #32 
                                  ($r (<RTLOP add> #5 (7, 16 #5)))
                                , FETCH_METHOD #32 
                                  (AGG-ID #32 ($w (<RTLOP add> #32 
                                        (<RTLOP sub> #32 
                                          (FETCH_METHOD #32 
                                            (AGG-ID #32 ($W (0 #1)))
                                          , 8 #32
                                          )
                                        , <RTLOP zx> #5 #32 7
                                        ))))
                                )
                              )
                            , SKIP
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          , ; 
            (--> 
              (<RTLOP ne> #5 (rd, <RTLOP add> #5 (0, 24 #5))
              , STORE_METHOD #32 
                (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (0, 24 #5)))
                , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                        (<RTLOP sub> #32 
                          (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 16 #32)
                        , <RTLOP zx> #5 #32 0
                        ))))
                )
              )
            , ; 
              (--> 
                (<RTLOP ne> #5 (rd, <RTLOP add> #5 (1, 24 #5))
                , STORE_METHOD #32 
                  (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (1, 24 #5)))
                  , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                          (<RTLOP sub> #32 
                            (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 16 #32
                            )
                          , <RTLOP zx> #5 #32 1
                          ))))
                  )
                )
              , ; 
                (--> 
                  (<RTLOP ne> #5 (rd, <RTLOP add> #5 (2, 24 #5))
                  , STORE_METHOD #32 
                    (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (2, 24 #5)))
                    , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                            (<RTLOP sub> #32 
                              (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                              , 16 #32
                              )
                            , <RTLOP zx> #5 #32 2
                            ))))
                    )
                  )
                , ; 
                  (--> 
                    (<RTLOP ne> #5 (rd, <RTLOP add> #5 (3, 24 #5))
                    , STORE_METHOD #32 
                      (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (3, 24 #5)))
                      , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                              (<RTLOP sub> #32 
                                (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                , 16 #32
                                )
                              , <RTLOP zx> #5 #32 3
                              ))))
                      )
                    )
                  , ; 
                    (--> 
                      (<RTLOP ne> #5 (rd, <RTLOP add> #5 (4, 24 #5))
                      , STORE_METHOD #32 
                        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (4, 24 #5)))
                        , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                                (<RTLOP sub> #32 
                                  (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                  , 16 #32
                                  )
                                , <RTLOP zx> #5 #32 4
                                ))))
                        )
                      )
                    , ; 
                      (--> 
                        (<RTLOP ne> #5 (rd, <RTLOP add> #5 (5, 24 #5))
                        , STORE_METHOD #32 
                          (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (5, 24 #5)))
                          , FETCH_METHOD #32 (AGG-ID #32 ($w (<RTLOP add> #32 
                                  (<RTLOP sub> #32 
                                    (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1)))
                                    , 16 #32
                                    )
                                  , <RTLOP zx> #5 #32 5
                                  ))))
                          )
                        )
                      , ; 
                        (--> 
                          (<RTLOP ne> #5 (rd, <RTLOP add> #5 (6, 24 #5))
                          , STORE_METHOD #32 
                            (AGG_METHOD #32 #32 
                              ($r (<RTLOP add> #5 (6, 24 #5)))
                            , FETCH_METHOD #32 
                              (AGG-ID #32 ($w (<RTLOP add> #32 
                                    (<RTLOP sub> #32 
                                      (FETCH_METHOD #32 
                                        (AGG-ID #32 ($W (0 #1)))
                                      , 16 #32
                                      )
                                    , <RTLOP zx> #5 #32 6
                                    ))))
                            )
                          )
                        , ; 
                          (--> 
                            (<RTLOP ne> #5 (rd, <RTLOP add> #5 (7, 24 #5))
                            , STORE_METHOD #32 
                              (AGG_METHOD #32 #32 
                                ($r (<RTLOP add> #5 (7, 24 #5)))
                              , FETCH_METHOD #32 
                                (AGG-ID #32 ($w (<RTLOP add> #32 
                                      (<RTLOP sub> #32 
                                        (FETCH_METHOD #32 
                                          (AGG-ID #32 ($W (0 #1)))
                                        , 16 #32
                                        )
                                      , <RTLOP zx> #5 #32 7
                                      ))))
                              )
                            )
                          , SKIP
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        , STORE_METHOD #32 
          (AGG-ID #32 ($W (0 #1))
          , <RTLOP sub> #32 
            (FETCH_METHOD #32 (AGG-ID #32 ($W (0 #1))), 16 #32)
          )
        )
      , STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      ) : rtl

default attribute of 
  andcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP and> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      , ; 
        (; 
          (; 
            (STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP lt> #32 
                  (<RTLOP and> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP eq> #32 
                  (<RTLOP and> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        , STORE_METHOD #1 
          (1-bits-at-loc #ungeneralized-8 #32 
            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
          , 0 #1
          )
        )
      ) : rtl

default attribute of 
  and (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP and> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      , SKIP
      ) : rtl

default attribute of 
  orcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP or> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      , ; 
        (; 
          (; 
            (STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP lt> #32 
                  (<RTLOP or> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP eq> #32 
                  (<RTLOP or> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        , STORE_METHOD #1 
          (1-bits-at-loc #ungeneralized-8 #32 
            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
          , 0 #1
          )
        )
      ) : rtl

default attribute of 
  or (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP or> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      , SKIP
      ) : rtl

default attribute of 
  xorcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP xor> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      , ; 
        (; 
          (; 
            (STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP lt> #32 
                  (<RTLOP xor> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP eq> #32 
                  (<RTLOP xor> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        , STORE_METHOD #1 
          (1-bits-at-loc #ungeneralized-8 #32 
            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
          , 0 #1
          )
        )
      ) : rtl

default attribute of 
  xor (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP xor> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
        )
      , SKIP
      ) : rtl

default attribute of 
  andncc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP and> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
          , <RTLOP com> #32 reg_or_imm
          )
        )
      , ; 
        (; 
          (; 
            (STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP lt> #32 
                  (<RTLOP and> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , <RTLOP com> #32 reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP eq> #32 
                  (<RTLOP and> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , <RTLOP com> #32 reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        , STORE_METHOD #1 
          (1-bits-at-loc #ungeneralized-8 #32 
            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
          , 0 #1
          )
        )
      ) : rtl

default attribute of 
  andn (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP and> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
          , <RTLOP com> #32 reg_or_imm
          )
        )
      , SKIP
      ) : rtl

default attribute of 
  orncc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP or> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
          , <RTLOP com> #32 reg_or_imm
          )
        )
      , ; 
        (; 
          (; 
            (STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP lt> #32 
                  (<RTLOP or> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , <RTLOP com> #32 reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP eq> #32 
                  (<RTLOP or> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , <RTLOP com> #32 reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        , STORE_METHOD #1 
          (1-bits-at-loc #ungeneralized-8 #32 
            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
          , 0 #1
          )
        )
      ) : rtl

default attribute of 
  orn (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP or> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
          , <RTLOP com> #32 reg_or_imm
          )
        )
      , SKIP
      ) : rtl

default attribute of 
  xnorcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP xor> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
          , <RTLOP com> #32 reg_or_imm
          )
        )
      , ; 
        (; 
          (; 
            (STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP lt> #32 
                  (<RTLOP xor> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , <RTLOP com> #32 reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP eq> #32 
                  (<RTLOP xor> #32 
                    (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                    , <RTLOP com> #32 reg_or_imm
                    )
                  , 0 #32
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        , STORE_METHOD #1 
          (1-bits-at-loc #ungeneralized-8 #32 
            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
          , 0 #1
          )
        )
      ) : rtl

default attribute of 
  xnor (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP xor> #32 
          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
          , <RTLOP com> #32 reg_or_imm
          )
        )
      , SKIP
      ) : rtl

default attribute of 
  add (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (<RTLOP add> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP eq> #1 
                    (1-bits-at #ungeneralized-12 #32 
                      (31 #ungeneralized-12
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-13 #32 
                      (31 #ungeneralized-13, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-14 #32 
                      (31 #ungeneralized-14
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-15 #32 
                      (31 #ungeneralized-15
                      , <RTLOP add> #32 
                        (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP carry> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  addcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (<RTLOP add> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP eq> #1 
                    (1-bits-at #ungeneralized-12 #32 
                      (31 #ungeneralized-12
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-13 #32 
                      (31 #ungeneralized-13, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-14 #32 
                      (31 #ungeneralized-14
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-15 #32 
                      (31 #ungeneralized-15
                      , <RTLOP add> #32 
                        (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP carry> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  addx (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (<RTLOP add> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP eq> #1 
                    (1-bits-at #ungeneralized-12 #32 
                      (31 #ungeneralized-12
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-13 #32 
                      (31 #ungeneralized-13, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-14 #32 
                      (31 #ungeneralized-14
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-15 #32 
                      (31 #ungeneralized-15
                      , <RTLOP add> #32 
                        (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (FETCH_METHOD #1 
                            (1-bits-at-loc #ungeneralized-8 #32 
                              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP carry> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                  (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3))))
              )
            )
          )
        )
      ) : rtl

default attribute of 
  addxcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (<RTLOP add> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP eq> #1 
                    (1-bits-at #ungeneralized-12 #32 
                      (31 #ungeneralized-12
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-13 #32 
                      (31 #ungeneralized-13, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-14 #32 
                      (31 #ungeneralized-14
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-15 #32 
                      (31 #ungeneralized-15
                      , <RTLOP add> #32 
                        (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (FETCH_METHOD #1 
                            (1-bits-at-loc #ungeneralized-8 #32 
                              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP carry> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                  (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3))))
              )
            )
          )
        )
      ) : rtl

default attribute of 
  umul (rs1, reg_or_imm, rd) is 
    ; 
      (; 
        (STORE_METHOD #32 
          (AGG-ID #32 ($i (3 #3))
          , 32-bits-at #ungeneralized-16 #ungeneralized-28 
            (32 #ungeneralized-16
            , <RTLOP mulUn> #32 #ungeneralized-28 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        , STORE_METHOD #32 
          (AGG_METHOD #32 #32 ($r rd)
          , 32-bits-at #ungeneralized-17 #ungeneralized-28 
            (0 #ungeneralized-17
            , <RTLOP mulUn> #32 #ungeneralized-28 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #ungeneralized-28 
                    (<RTLOP mulUn> #32 #ungeneralized-28 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-28
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #ungeneralized-28 
                    (<RTLOP mulUn> #32 #ungeneralized-28 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-28
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP undefined> #1
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP undefined> #1
            )
          )
        )
      ) : rtl

default attribute of 
  umulcc (rs1, reg_or_imm, rd) is 
    ; 
      (; 
        (STORE_METHOD #32 
          (AGG-ID #32 ($i (3 #3))
          , 32-bits-at #ungeneralized-16 #ungeneralized-29 
            (32 #ungeneralized-16
            , <RTLOP mulUn> #32 #ungeneralized-29 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        , STORE_METHOD #32 
          (AGG_METHOD #32 #32 ($r rd)
          , 32-bits-at #ungeneralized-17 #ungeneralized-29 
            (0 #ungeneralized-17
            , <RTLOP mulUn> #32 #ungeneralized-29 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #ungeneralized-29 
                    (<RTLOP mulUn> #32 #ungeneralized-29 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-29
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #ungeneralized-29 
                    (<RTLOP mulUn> #32 #ungeneralized-29 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-29
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP undefined> #1
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP undefined> #1
            )
          )
        )
      ) : rtl

default attribute of 
  smul (rs1, reg_or_imm, rd) is 
    ; 
      (; 
        (STORE_METHOD #32 
          (AGG-ID #32 ($i (3 #3))
          , 32-bits-at #ungeneralized-16 #ungeneralized-30 
            (32 #ungeneralized-16
            , <RTLOP mul> #32 #ungeneralized-30 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        , STORE_METHOD #32 
          (AGG_METHOD #32 #32 ($r rd)
          , 32-bits-at #ungeneralized-17 #ungeneralized-30 
            (0 #ungeneralized-17
            , <RTLOP mul> #32 #ungeneralized-30 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #ungeneralized-30 
                    (<RTLOP mul> #32 #ungeneralized-30 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-30
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #ungeneralized-30 
                    (<RTLOP mul> #32 #ungeneralized-30 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-30
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP undefined> #1
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP undefined> #1
            )
          )
        )
      ) : rtl

default attribute of 
  smulcc (rs1, reg_or_imm, rd) is 
    ; 
      (; 
        (STORE_METHOD #32 
          (AGG-ID #32 ($i (3 #3))
          , 32-bits-at #ungeneralized-16 #ungeneralized-31 
            (32 #ungeneralized-16
            , <RTLOP mul> #32 #ungeneralized-31 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        , STORE_METHOD #32 
          (AGG_METHOD #32 #32 ($r rd)
          , 32-bits-at #ungeneralized-17 #ungeneralized-31 
            (0 #ungeneralized-17
            , <RTLOP mul> #32 #ungeneralized-31 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
            )
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #ungeneralized-31 
                    (<RTLOP mul> #32 #ungeneralized-31 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-31
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #ungeneralized-31 
                    (<RTLOP mul> #32 #ungeneralized-31 
                      (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      , reg_or_imm
                      )
                    , 0 #ungeneralized-31
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP undefined> #1
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP undefined> #1
            )
          )
        )
      ) : rtl

default attribute of 
  ba (target, annul) is 
    --> 
      (<RTLOP bool> (1 #1), STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bn (target, annul) is 
    --> 
      (<RTLOP bool> (0 #1), STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bne (target, annul) is 
    --> 
      (<RTLOP bool> 
        (<RTLOP com> #1 (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-6 #32 
              (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3))))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  be (target, annul) is 
    --> 
      (<RTLOP bool> (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-6 #32 
            (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bg (target, annul) is 
    --> 
      (<RTLOP bool> (<RTLOP com> #1 (<RTLOP or> #1 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3))))
            , <RTLOP xor> #1 
              (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))
              , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
                  (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))
              )
            )))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  ble (target, annul) is 
    --> 
      (<RTLOP bool> (<RTLOP or> #1 
          (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-6 #32 
              (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3))))
          , <RTLOP xor> #1 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))
            , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))
            )
          ))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bge (target, annul) is 
    --> 
      (<RTLOP bool> (<RTLOP com> #1 (<RTLOP xor> #1 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))
            , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))
            )))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bl (target, annul) is 
    --> 
      (<RTLOP bool> (<RTLOP xor> #1 
          (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
              (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))
          , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))
          ))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bgu (target, annul) is 
    --> 
      (<RTLOP bool> (<RTLOP com> #1 (<RTLOP or> #1 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3))))
            , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-6 #32 
                (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3))))
            )))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bleu (target, annul) is 
    --> 
      (<RTLOP bool> (<RTLOP or> #1 
          (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3))))
          , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-6 #32 
              (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3))))
          ))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bcc (target, annul) is 
    --> 
      (<RTLOP bool> 
        (<RTLOP com> #1 (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3))))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bcs (target, annul) is 
    --> 
      (<RTLOP bool> (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bpos (target, annul) is 
    --> 
      (<RTLOP bool> 
        (<RTLOP com> #1 (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
              (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bneg (target, annul) is 
    --> 
      (<RTLOP bool> (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
            (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bvc (target, annul) is 
    --> 
      (<RTLOP bool> 
        (<RTLOP com> #1 (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
              (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  bvs (target, annul) is 
    --> 
      (<RTLOP bool> (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
            (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))))
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  call target is 
    ; 
      (STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      , STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r (<RTLOP add> #5 (7 #5, 8 #5)))
        , FETCH_METHOD #32 (AGG-ID #32 ($i (4 #3)))
        )
      ) : rtl

default attribute of 
  jmpl (address, rd) is 
    ; 
      (STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), address)
      , STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd), FETCH_METHOD #32 (AGG-ID #32 ($i (4 #3)))
        )
      ) : rtl

default attribute of 
  ldf (address, fd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($f fd)
      , FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address))
      ) : rtl

default attribute of 
  lddf (address, fd) is 
    STORE_METHOD #64 
      (AGG_METHOD #32 #64 ($f fd)
      , FETCH_METHOD #64 (AGG_METHOD #8 #64 ($m address))
      ) : rtl

default attribute of 
  ldfsr address is 
    STORE_METHOD #32 
      (AGG-ID #32 ($F (0 #1))
      , FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address))
      ) : rtl

default attribute of 
  ldc (address, cd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($c cd)
      , FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address))
      ) : rtl

default attribute of 
  lddc (address, cd) is 
    STORE_METHOD #64 
      (AGG_METHOD #32 #64 ($c cd)
      , FETCH_METHOD #64 (AGG_METHOD #8 #64 ($m address))
      ) : rtl

default attribute of 
  ldcsr address is 
    STORE_METHOD #32 
      (AGG-ID #32 ($C (0 #1))
      , FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address))
      ) : rtl

default attribute of 
  stf (fd, address) is 
    STORE_METHOD #32 
      (AGG_METHOD #8 #32 ($m address)
      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($f fd))
      ) : rtl

default attribute of 
  stdf (fd, address) is 
    STORE_METHOD #64 
      (AGG_METHOD #8 #64 ($m address)
      , FETCH_METHOD #64 (AGG_METHOD #32 #64 ($f fd))
      ) : rtl

default attribute of 
  stfsr address is 
    STORE_METHOD #32 
      (AGG_METHOD #8 #32 ($m address)
      , FETCH_METHOD #32 (AGG-ID #32 ($F (0 #1)))
      ) : rtl

default attribute of 
  stc (cd, address) is 
    STORE_METHOD #32 
      (AGG_METHOD #8 #32 ($m address)
      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($c cd))
      ) : rtl

default attribute of 
  stdc (cd, address) is 
    STORE_METHOD #64 
      (AGG_METHOD #8 #64 ($m address)
      , FETCH_METHOD #64 (AGG_METHOD #32 #64 ($c cd))
      ) : rtl

default attribute of 
  stcsr address is 
    STORE_METHOD #32 
      (AGG_METHOD #8 #32 ($m address)
      , FETCH_METHOD #32 (AGG-ID #32 ($C (0 #1)))
      ) : rtl

default attribute of 
  ldnext (fd, address) is 
    STORE_METHOD #32 
      (32-bits-at-loc #ungeneralized-32 #64 
        (0 #ungeneralized-32, AGG_METHOD #32 #64 ($f fd))
      , FETCH_METHOD #32 (AGG_METHOD #8 #32 ($m address))
      ) : rtl

default attribute of 
  stnext (fd, address) is 
    STORE_METHOD #32 
      (AGG_METHOD #8 #32 ($m address)
      , 32-bits-at #ungeneralized-33 #64 
        (0 #ungeneralized-33, FETCH_METHOD #64 (AGG_METHOD #32 #64 ($f fd)))
      ) : rtl

default attribute of 
  sethi (imm22, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP bitInsert> #ungeneralized-34 #32 #22 
        ({wide is 0 #32, lsb is 10 #ungeneralized-34}, imm22)
      ) : rtl

default attribute of 
  sll (rs1, reg_or_imm, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP lshift> #5 #32 
        (32 #5
        , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
        , 5-bits-at #ungeneralized-35 #32 (0 #ungeneralized-35, reg_or_imm)
        )
      ) : rtl

default attribute of 
  srl (rs1, reg_or_imm, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP rshift> #5 #32 
        (32 #5
        , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
        , 5-bits-at #ungeneralized-36 #32 (0 #ungeneralized-36, reg_or_imm)
        )
      ) : rtl

default attribute of 
  sra (rs1, reg_or_imm, rd) is 
    STORE_METHOD #32 
      (AGG_METHOD #32 #32 ($r rd)
      , <RTLOP rshiftA> #5 #32 
        (32 #5
        , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
        , 5-bits-at #ungeneralized-37 #32 (0 #ungeneralized-37, reg_or_imm)
        )
      ) : rtl

default attribute of 
  taddcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (<RTLOP add> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP eq> #1 
                    (1-bits-at #ungeneralized-12 #32 
                      (31 #ungeneralized-12
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-13 #32 
                      (31 #ungeneralized-13, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-14 #32 
                      (31 #ungeneralized-14
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-15 #32 
                      (31 #ungeneralized-15
                      , <RTLOP add> #32 
                        (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP carry> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  taddcctv (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP add> #32 
          (<RTLOP add> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP eq> #1 
                    (1-bits-at #ungeneralized-12 #32 
                      (31 #ungeneralized-12
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-13 #32 
                      (31 #ungeneralized-13, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-14 #32 
                      (31 #ungeneralized-14
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-15 #32 
                      (31 #ungeneralized-15
                      , <RTLOP add> #32 
                        (<RTLOP add> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP carry> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  sub (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP sub> #32 
          (<RTLOP sub> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP ne> #1 
                    (1-bits-at #ungeneralized-22 #32 
                      (31 #ungeneralized-22
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-23 #32 
                      (31 #ungeneralized-23, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-24 #32 
                      (31 #ungeneralized-24
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-25 #32 
                      (31 #ungeneralized-25
                      , <RTLOP sub> #32 
                        (<RTLOP sub> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP borrow> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  subcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP sub> #32 
          (<RTLOP sub> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP ne> #1 
                    (1-bits-at #ungeneralized-22 #32 
                      (31 #ungeneralized-22
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-23 #32 
                      (31 #ungeneralized-23, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-24 #32 
                      (31 #ungeneralized-24
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-25 #32 
                      (31 #ungeneralized-25
                      , <RTLOP sub> #32 
                        (<RTLOP sub> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP borrow> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  subx (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP sub> #32 
          (<RTLOP sub> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP ne> #1 
                    (1-bits-at #ungeneralized-22 #32 
                      (31 #ungeneralized-22
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-23 #32 
                      (31 #ungeneralized-23, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-24 #32 
                      (31 #ungeneralized-24
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-25 #32 
                      (31 #ungeneralized-25
                      , <RTLOP sub> #32 
                        (<RTLOP sub> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (FETCH_METHOD #1 
                            (1-bits-at-loc #ungeneralized-8 #32 
                              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP borrow> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                  (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3))))
              )
            )
          )
        )
      ) : rtl

default attribute of 
  subxcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP sub> #32 
          (<RTLOP sub> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 
            (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 
                        (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                            (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP ne> #1 
                    (1-bits-at #ungeneralized-22 #32 
                      (31 #ungeneralized-22
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-23 #32 
                      (31 #ungeneralized-23, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-24 #32 
                      (31 #ungeneralized-24
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-25 #32 
                      (31 #ungeneralized-25
                      , <RTLOP sub> #32 
                        (<RTLOP sub> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (FETCH_METHOD #1 
                            (1-bits-at-loc #ungeneralized-8 #32 
                              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))))
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP borrow> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-8 #32 
                  (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3))))
              )
            )
          )
        )
      ) : rtl

default attribute of 
  tsubcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP sub> #32 
          (<RTLOP sub> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP ne> #1 
                    (1-bits-at #ungeneralized-22 #32 
                      (31 #ungeneralized-22
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-23 #32 
                      (31 #ungeneralized-23, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-24 #32 
                      (31 #ungeneralized-24
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-25 #32 
                      (31 #ungeneralized-25
                      , <RTLOP sub> #32 
                        (<RTLOP sub> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP borrow> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  tsubcctv (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP sub> #32 
          (<RTLOP sub> #32 
            (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)), reg_or_imm)
          , <RTLOP zx> #1 #32 (0 #1)
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP sub> #32 
                      (<RTLOP sub> #32 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , reg_or_imm
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP ne> #1 
                    (1-bits-at #ungeneralized-22 #32 
                      (31 #ungeneralized-22
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-23 #32 
                      (31 #ungeneralized-23, reg_or_imm)
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-24 #32 
                      (31 #ungeneralized-24
                      , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                      )
                    , 1-bits-at #ungeneralized-25 #32 
                      (31 #ungeneralized-25
                      , <RTLOP sub> #32 
                        (<RTLOP sub> #32 
                          (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                          , reg_or_imm
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP borrow> #32 
              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
              , reg_or_imm
              , 0 #1
              )
            )
          )
        )
      ) : rtl

default attribute of 
  mulscc (rs1, reg_or_imm, rd) is 
    ; 
      (; 
        (STORE_METHOD #32 
          (AGG_METHOD #32 #32 ($r rd)
          , <RTLOP add> #32 
            (<RTLOP add> #32 
              (reg_or_imm
              , if <RTLOP eq> #1 
                    (1-bits-at #ungeneralized-40 #32 
                      (0 #ungeneralized-40
                      , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                      )
                    , 0 #1
                    ) 
              then 
                0 #32 
              else 
                <RTLOP bitInsert> #ungeneralized-38 #32 #1 
                  (
                  {wide is 
                      <RTLOP rshift> #ungeneralized-39 #32 
                        (32 #ungeneralized-39
                        , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , 1 #ungeneralized-39
                        )
                  , lsb is 31 #ungeneralized-38
                  }
                  , <RTLOP xor> #1 
                    (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
                        (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))
                    , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
                        (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))
                    )
                  ) 
              fi
              )
            , <RTLOP zx> #1 #32 (0 #1)
            )
          )
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (reg_or_imm
                        , if <RTLOP eq> #1 
                              (1-bits-at #ungeneralized-40 #32 
                                (0 #ungeneralized-40
                                , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                                )
                              , 0 #1
                              ) 
                        then 
                          0 #32 
                        else 
                          <RTLOP bitInsert> #ungeneralized-38 #32 #1 
                            (
                            {wide is 
                                <RTLOP rshift> #ungeneralized-39 #32 
                                  (32 #ungeneralized-39
                                  , FETCH_METHOD #32 
                                    (AGG_METHOD #32 #32 ($r rs1))
                                  , 1 #ungeneralized-39
                                  )
                            , lsb is 31 #ungeneralized-38
                            }
                            , <RTLOP xor> #1 
                              (FETCH_METHOD #1 
                                (1-bits-at-loc #ungeneralized-5 #32 
                                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))
                                  ))
                              , FETCH_METHOD #1 
                                (1-bits-at-loc #ungeneralized-7 #32 
                                  (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))
                                  ))
                              )
                            ) 
                        fi
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP add> #32 
                      (<RTLOP add> #32 
                        (reg_or_imm
                        , if <RTLOP eq> #1 
                              (1-bits-at #ungeneralized-40 #32 
                                (0 #ungeneralized-40
                                , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                                )
                              , 0 #1
                              ) 
                        then 
                          0 #32 
                        else 
                          <RTLOP bitInsert> #ungeneralized-38 #32 #1 
                            (
                            {wide is 
                                <RTLOP rshift> #ungeneralized-39 #32 
                                  (32 #ungeneralized-39
                                  , FETCH_METHOD #32 
                                    (AGG_METHOD #32 #32 ($r rs1))
                                  , 1 #ungeneralized-39
                                  )
                            , lsb is 31 #ungeneralized-38
                            }
                            , <RTLOP xor> #1 
                              (FETCH_METHOD #1 
                                (1-bits-at-loc #ungeneralized-5 #32 
                                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))
                                  ))
                              , FETCH_METHOD #1 
                                (1-bits-at-loc #ungeneralized-7 #32 
                                  (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))
                                  ))
                              )
                            ) 
                        fi
                        )
                      , <RTLOP zx> #1 #32 (0 #1)
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP bit> (<RTLOP andalso> 
                  (<RTLOP eq> #1 
                    (1-bits-at #ungeneralized-12 #32 
                      (31 #ungeneralized-12, reg_or_imm)
                    , 1-bits-at #ungeneralized-13 #32 
                      (31 #ungeneralized-13
                      , if <RTLOP eq> #1 
                            (1-bits-at #ungeneralized-40 #32 
                              (0 #ungeneralized-40
                              , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                              )
                            , 0 #1
                            ) 
                      then 
                        0 #32 
                      else 
                        <RTLOP bitInsert> #ungeneralized-38 #32 #1 
                          (
                          {wide is 
                              <RTLOP rshift> #ungeneralized-39 #32 
                                (32 #ungeneralized-39
                                , FETCH_METHOD #32 
                                  (AGG_METHOD #32 #32 ($r rs1))
                                , 1 #ungeneralized-39
                                )
                          , lsb is 31 #ungeneralized-38
                          }
                          , <RTLOP xor> #1 
                            (FETCH_METHOD #1 
                              (1-bits-at-loc #ungeneralized-5 #32 
                                (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))
                            , FETCH_METHOD #1 
                              (1-bits-at-loc #ungeneralized-7 #32 
                                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))
                            )
                          ) 
                      fi
                      )
                    )
                  , <RTLOP ne> #1 
                    (1-bits-at #ungeneralized-14 #32 
                      (31 #ungeneralized-14, reg_or_imm)
                    , 1-bits-at #ungeneralized-15 #32 
                      (31 #ungeneralized-15
                      , <RTLOP add> #32 
                        (<RTLOP add> #32 
                          (reg_or_imm
                          , if <RTLOP eq> #1 
                                (1-bits-at #ungeneralized-40 #32 
                                  (0 #ungeneralized-40
                                  , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                                  )
                                , 0 #1
                                ) 
                          then 
                            0 #32 
                          else 
                            <RTLOP bitInsert> #ungeneralized-38 #32 #1 
                              (
                              {wide is 
                                  <RTLOP rshift> #ungeneralized-39 #32 
                                    (32 #ungeneralized-39
                                    , FETCH_METHOD #32 
                                      (AGG_METHOD #32 #32 ($r rs1))
                                    , 1 #ungeneralized-39
                                    )
                              , lsb is 31 #ungeneralized-38
                              }
                              , <RTLOP xor> #1 
                                (FETCH_METHOD #1 
                                  (1-bits-at-loc #ungeneralized-5 #32 
                                    (23 #ungeneralized-5
                                    , AGG-ID #32 ($i (0 #3))
                                    ))
                                , FETCH_METHOD #1 
                                  (1-bits-at-loc #ungeneralized-7 #32 
                                    (21 #ungeneralized-7
                                    , AGG-ID #32 ($i (0 #3))
                                    ))
                                )
                              ) 
                          fi
                          )
                        , <RTLOP zx> #1 #32 (0 #1)
                        )
                      )
                    )
                  ))
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , <RTLOP carry> #32 
              (reg_or_imm
              , if <RTLOP eq> #1 
                    (1-bits-at #ungeneralized-40 #32 
                      (0 #ungeneralized-40
                      , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                      )
                    , 0 #1
                    ) 
              then 
                0 #32 
              else 
                <RTLOP bitInsert> #ungeneralized-38 #32 #1 
                  (
                  {wide is 
                      <RTLOP rshift> #ungeneralized-39 #32 
                        (32 #ungeneralized-39
                        , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
                        , 1 #ungeneralized-39
                        )
                  , lsb is 31 #ungeneralized-38
                  }
                  , <RTLOP xor> #1 
                    (FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-5 #32 
                        (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3))))
                    , FETCH_METHOD #1 (1-bits-at-loc #ungeneralized-7 #32 
                        (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3))))
                    )
                  ) 
              fi
              , 0 #1
              )
            )
          )
        )
      , STORE_METHOD #32 
        (AGG-ID #32 ($i (3 #3))
        , <RTLOP bitInsert> #ungeneralized-38 #32 #1 
          (
          {wide is 
              <RTLOP rshift> #ungeneralized-39 #32 
                (32 #ungeneralized-39
                , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                , 1 #ungeneralized-39
                )
          , lsb is 31 #ungeneralized-38
          }
          , 1-bits-at #ungeneralized-41 #32 
            (0 #ungeneralized-41
            , FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1))
            )
          )
        )
      ) : rtl

default attribute of 
  udiv (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP divRz> #64 #32 
          (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
            (
            {wide is 
                <RTLOP zx> #32 #64 
                  (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
            , lsb is 32 #ungeneralized-18
            }
            , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
            )
          , reg_or_imm
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP divRz> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP divRz> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP sparc_sdiv_overflow> 
                (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                  (
                  {wide is 
                      <RTLOP zx> #32 #64 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                  , lsb is 32 #ungeneralized-18
                  }
                  , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                  )
                , reg_or_imm
                )
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        )
      ) : rtl

default attribute of 
  udivcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP divRz> #64 #32 
          (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
            (
            {wide is 
                <RTLOP zx> #32 #64 
                  (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
            , lsb is 32 #ungeneralized-18
            }
            , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
            )
          , reg_or_imm
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP divRz> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP divRz> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP sparc_sdiv_overflow> 
                (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                  (
                  {wide is 
                      <RTLOP zx> #32 #64 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                  , lsb is 32 #ungeneralized-18
                  }
                  , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                  )
                , reg_or_imm
                )
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        )
      ) : rtl

default attribute of 
  sdiv (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP divUn> #64 #32 
          (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
            (
            {wide is 
                <RTLOP zx> #32 #64 
                  (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
            , lsb is 32 #ungeneralized-18
            }
            , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
            )
          , reg_or_imm
          )
        )
      , --> 
        (FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP divUn> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP divUn> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP sparc_udiv_overflow> 
                (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                  (
                  {wide is 
                      <RTLOP zx> #32 #64 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                  , lsb is 32 #ungeneralized-18
                  }
                  , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                  )
                , reg_or_imm
                )
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        )
      ) : rtl

default attribute of 
  sdivcc (rs1, reg_or_imm, rd) is 
    ; 
      (STORE_METHOD #32 
        (AGG_METHOD #32 #32 ($r rd)
        , <RTLOP divUn> #64 #32 
          (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
            (
            {wide is 
                <RTLOP zx> #32 #64 
                  (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
            , lsb is 32 #ungeneralized-18
            }
            , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
            )
          , reg_or_imm
          )
        )
      , --> 
        (NOT FALSE
        , ; 
          (; 
            (; 
              (STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-5 #32 
                  (23 #ungeneralized-5, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP lt> #32 
                    (<RTLOP divUn> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              , STORE_METHOD #1 
                (1-bits-at-loc #ungeneralized-6 #32 
                  (22 #ungeneralized-6, AGG-ID #32 ($i (0 #3)))
                , <RTLOP bit> (<RTLOP eq> #32 
                    (<RTLOP divUn> #64 #32 
                      (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                        (
                        {wide is 
                            <RTLOP zx> #32 #64 
                              (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                        , lsb is 32 #ungeneralized-18
                        }
                        , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                        )
                      , reg_or_imm
                      )
                    , 0 #32
                    ))
                )
              )
            , STORE_METHOD #1 
              (1-bits-at-loc #ungeneralized-7 #32 
                (21 #ungeneralized-7, AGG-ID #32 ($i (0 #3)))
              , <RTLOP sparc_udiv_overflow> 
                (<RTLOP bitInsert> #ungeneralized-18 #64 #32 
                  (
                  {wide is 
                      <RTLOP zx> #32 #64 
                        (FETCH_METHOD #32 (AGG_METHOD #32 #32 ($r rs1)))
                  , lsb is 32 #ungeneralized-18
                  }
                  , FETCH_METHOD #32 (AGG-ID #32 ($i (3 #3)))
                  )
                , reg_or_imm
                )
              )
            )
          , STORE_METHOD #1 
            (1-bits-at-loc #ungeneralized-8 #32 
              (20 #ungeneralized-8, AGG-ID #32 ($i (0 #3)))
            , 0 #1
            )
          )
        )
      ) : rtl

default attribute of 
  fba (target, annul) is 
    --> (NOT FALSE, STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)) : rtl

default attribute of 
  fbn (target, annul) is 
    --> (FALSE, STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)) : rtl

default attribute of 
  fbu (target, annul) is 
    --> 
      (<RTLOP eq> #2 
        (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
            (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
        , <RTLOP unordered>
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbg (target, annul) is 
    --> 
      (<RTLOP eq> #2 
        (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
            (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
        , <RTLOP float_gt>
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbug (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_gt>
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP unordered>
          )
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbl (target, annul) is 
    --> 
      (<RTLOP eq> #2 
        (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
            (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
        , <RTLOP float_lt>
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbul (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_lt>
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP unordered>
          )
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fblg (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_lt>
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_gt>
          )
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbne (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP orelse> 
          (<RTLOP eq> #2 
            (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
                (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
            , <RTLOP float_lt>
            )
          , <RTLOP eq> #2 
            (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
                (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
            , <RTLOP float_gt>
            )
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP unordered>
          )
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbe (target, annul) is 
    --> 
      (<RTLOP eq> #2 
        (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
            (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
        , <RTLOP float_eq>
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbue (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_eq>
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP unordered>
          )
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbge (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_eq>
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_gt>
          )
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fbuge (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP orelse> 
          (<RTLOP eq> #2 
            (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
                (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
            , <RTLOP float_eq>
            )
          , <RTLOP eq> #2 
            (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
                (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
            , <RTLOP float_gt>
            )
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP unordered>
          )
        )
      , STORE_METHOD #32 (AGG-ID #32 ($i (5 #3)), target)
      ) : rtl

default attribute of 
  fble (target, annul) is 
    --> 
      (<RTLOP orelse> 
        (<RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralized-10, AGG-ID #32 ($F (0 #1))))
          , <RTLOP float_eq>
          )
        , <RTLOP eq> #2 
          (FETCH_METHOD #2 (2-bits-at-loc #ungeneralized-10 #32 
              (10 #ungeneralize