We present software for designing Totally Self Checking Sequential Machines. We restrict our considerations to sequential circuits with inputs, internal states and outputs encoded with any unordered code. We propose theorems to verify self testing (ST) and code-disjoin (CD) properties. Circuits tested as not ST or/and CD are modified to obtain those properties. We also propose a method for internal states encoding which guarantees ST of Self Testing Checker (STC) circuit for internal states code. Owing to our methods we can design TSC circuits in a fully automatic way.