Translating Concurrent Action Oriented Specifications to Synchronous Guarded Actions

摘要

Concurrent Action-Oriented Specifications (CAOS) model the behavior of a synchronous hardware circuit as asynchronous guarded actions at an abstraction level higher than the Register Transfer Level (RTL). Previous approaches always considered the compilation of CAOS, which includes a transformation of the underlying model of computation and the scheduling of guarded actions per clock cycle, as a tightly integrated step. In this paper, we present a new compilation procedure, which separates these two tasks and translates CAOS models to synchronous guarded actions with an explicit interface to a scheduler. This separation of concerns has many advantages, including better analyses and integration of custom schedulers. Our method also generates assertions that each scheduler must obey that can be fulfilled by algorithms for scheduler synthesis like those developed in supervisory control. We present our translation procedure in detail and illustrate it by various examples. We also show that our method simplifies formal verification of hardware synthesized from CAOS specifications over previously known formal verification approaches.