db_ppc4xx_dumptlb
{ DDB_ADD_CMD("tlb", db_ppc4xx_dumptlb, 0,
static void db_ppc4xx_dumptlb(db_expr_t, bool, db_expr_t, const char *);