This paper proposes a state encoding method for asynchronous circuits based on the theory of regions. A region in a Transition System is a set of states that "behave uniformly" with respect to a given transition (value change of an observable signal), and is analogue to a place in a Petri net. Regions are tightly connected with a set of properties that must be preserved across the state encoding process, namely: (1) trace equivalence between the original and the encoded specification, and (2) implementability as a speedindependent circuit. We build on a theoretical body of work that has shown the significance of regions for such property-preserving transformations, and describe a set of algorithms aimed at efficiently solving the encoding problem. The algorithms have been implemented in a software tool called petrify. Unlike many existing tools, petrify represents the encoded specification as an STG, and thus allows the designer to be more closely involved in the synthesis p...