RTL generation of channel architecture templates for a template-based SoC design flow

In this paper, we propose the design methodology for communication channel templates from formal specification to RTL description. In this flow, design and verification start from one source, LTL property. We constructed LTL-to-TRS, which is translator from LTL property sets to Bluespec term-rewriting system (TRS) description. And, we use a Bluespec compiler as a synthesizer from TRS to RTL. Also, to match the implementation with the formal specification, we use a VIS solver as a model checker. And then, channel instances generated by proposed design method are transformed into channel template-generators for communication channel library. These channel templates can be used in DSE process in SoC design flow.