6 files changed, 15 insertions, 23 deletions
diff --git a/pk/gpe/gpe_timebase.h b/pk/gpe/gpe_timebase.h
index 3c27bdfb..648a3dcd 100644
--- a/pk/gpe/gpe_timebase.h
+++ b/pk/gpe/gpe_timebase.h
@@ -15,13 +15,9 @@
 
 #include "pk.h"
 
-//The timebase register is not yet supported in the OCB model.
-//remove this line once it is supported.
-#define APPCFG_USE_DEC_FOR_TIMEBASE
-
 #ifndef __ASSEMBLER__
 
-#ifndef APPCFG_USE_DEC_FOR_TIMEBASE
+#ifdef APPCFG_USE_EXT_TIMEBASE
 static inline
 uint32_t pk_timebase32_get(void)
 {
@@ -32,7 +28,7 @@ uint32_t pk_timebase32_get(void)
 //assembly function is defined in ppe42_timebase.S
 uint32_t pk_timebase32_get(void);
 
-#endif /* APPCFG_USE_DEC_FOR_TIMEBASE */
+#endif /* APPCFG_USE_EXT_TIMEBASE */
 
 #else
 
diff --git a/pk/ppe/ppe_timebase.h b/pk/ppe/ppe_timebase.h
index f3d2c91d..45da0080 100644
--- a/pk/ppe/ppe_timebase.h
+++ b/pk/ppe/ppe_timebase.h
@@ -7,16 +7,16 @@
 // *! *** IBM Confidential ***
 //-----------------------------------------------------------------------------
 
-/// \file gpe_timebase.h
+/// \file ppe_timebase.h
 /// \brief support for using the OCB 32 bit timebase register
 ///
-/// The OCB timebase register is a 32 bit count-up register that is shared
-/// by all GPE's in the OCC complex.
 
 #include "pk.h"
 
 //The timebase register will never be supported in the base ppe model
-#define APPCFG_USE_DEC_FOR_TIMEBASE
+#ifdef APPCFG_USE_EXT_TIMEBASE
+#error "External timebase is not supported on the PPE standalone model"
+#endif /* APPCFG_USE_EXT_TIMEBASE */
 
 #ifndef __ASSEMBLER__
 
diff --git a/pk/ppe42/ppe42_core.c b/pk/ppe42/ppe42_core.c
index 6586888c..b49b8855 100644
--- a/pk/ppe42/ppe42_core.c
+++ b/pk/ppe42/ppe42_core.c
@@ -102,7 +102,7 @@ pk_interrupt_preemption_disable()
 // If the \a timeout is in the past, we schedule the PIT interrupt for 1 tick
 // in the future in accordance with the PK specification.
 
-#ifdef APPCFG_USE_DEC_FOR_TIMEBASE
+#ifndef APPCFG_USE_EXT_TIMEBASE
 void
 __pk_schedule_hardware_timeout(PkTimebase timeout)
 {
@@ -180,7 +180,7 @@ __pk_schedule_hardware_timeout(PkTimebase timeout)
     }
 }
 
-#endif  /* APPCFG_USE_DEC_FOR_TIMEBASE */
+#endif  /* APPCFG_USE_EXT_TIMEBASE */
 
 #endif  /* PK_TIMER_SUPPORT */
 
diff --git a/pk/ppe42/ppe42_init.c b/pk/ppe42/ppe42_init.c
index 0beea37d..52659aab 100644
--- a/pk/ppe42/ppe42_init.c
+++ b/pk/ppe42/ppe42_init.c
@@ -53,13 +53,13 @@ __ppe42_system_setup()
     //Clear all status bits in the TSR
     mtspr(SPRN_TSR, TSR_ENW | TSR_WIS | TSR_DIS | TSR_FIS);
 
-#ifndef APPCFG_USE_DEC_FOR_TIMEBASE
+#ifdef APPCFG_USE_EXT_TIMEBASE
     //Enable the DEC interrupt and configure it to use the external dec_timer signal
     mtspr(SPRN_TCR, TCR_DIE | TCR_DS);
 #else
     //Enable the DEC interrupt and configure it to use the internal clock signal
     mtspr(SPRN_TCR, TCR_DIE);
-#endif /* APPCFG_USE_DEC_FOR_TIMEBASE */
+#endif /* APPCFG_USE_EXT_TIMEBASE */
 
 #if PK_TIMER_SUPPORT
 #if PK_TRACE_SUPPORT
diff --git a/pk/ppe42/ppe42_timebase.S b/pk/ppe42/ppe42_timebase.S
index 43d64bb4..54d28fa1 100644
--- a/pk/ppe42/ppe42_timebase.S
+++ b/pk/ppe42/ppe42_timebase.S
@@ -23,7 +23,7 @@ pk_timebase_get(void);
         .global ppe42_tb_data
         .global_function pk_timebase_get
 
-#ifdef APPCFG_USE_DEC_FOR_TIMEBASE
+#ifndef APPCFG_USE_EXT_TIMEBASE
 
         /// Note that it is ok to use this function in a fast interrupt
         /// context
@@ -102,7 +102,7 @@ pk_timebase_get:
         _pk_timebase32_get r5, r5
 
         //increment the upper 32 bits if the lower 32 bits have flipped
-        cmplwbgt r5, r4, update_lower_32
+        cmplwbge r5, r4, update_lower_32
 
         //increment the upper 32 bits
         addi        r3, r3, 1
@@ -112,5 +112,5 @@ update_lower_32:
         mr          r4, r5
 
         blr
-#endif
+#endif /* APPCFG_USE_EXT_TIMEBASE */
 /// \endcond
diff --git a/pk/std/std_timebase.h b/pk/std/std_timebase.h
index e88a9bc6..855320d5 100644
--- a/pk/std/std_timebase.h
+++ b/pk/std/std_timebase.h
@@ -15,13 +15,9 @@
 
 #include "pk.h"
 
-//The timebase register is not yet supported in the STD model.
-//remove this line once it is supported.
-#define APPCFG_USE_DEC_FOR_TIMEBASE
-
 #ifndef __ASSEMBLER__
 
-#ifndef APPCFG_USE_DEC_FOR_TIMEBASE
+#ifndef APPCFG_USE_EXT_TIMEBASE
 static inline
 uint32_t pk_timebase32_get(void)
 {
@@ -32,7 +28,7 @@ uint32_t pk_timebase32_get(void)
 //assembly function is defined in ppe42_timebase.S
 uint32_t pk_timebase32_get(void);
 
-#endif  /* APPCFG_USE_DEC_FOR_TIMEBASE */
+#endif  /* APPCFG_USE_EXT_TIMEBASE */
 
 #else