Formal specification of an asynchronous Viterbi decoder

Conventionally, the correctness of functional and nonfunctional properties of hardware components is ensured during design process by simulation. Moreover, different description languages are needed during development phases. Thus, by adopting the action systems, we are able to use the same formalism from specification down to implementation. Recently, we have been exploiting possibilities to formally model power consumption. That is the purpose is to develop a formal power estimation flow which can be used to monitor the power consumption from abstract level down to the gate level implementation. In this paper, we present a formal model for asynchronous Viterbi decoder, which will be used as a case study for the power estimation flow in the future.