Architectural system modeling for correct-by-construction RTL design

This paper works towards a new design flow in which a design model at an architectural system level is refined into an RTL implementation in such a way that architectural model and RTL implementation stand in a well-defined formal relationship to each other. Functional properties valid at the system level are guaranteed to hold also in the concrete implementation without any additional verification efforts at the RTL. Based on the notion of path predicate abstraction (PPA) introduced in previous work, this paper contributes an "architectural modeling language (AML)" which formalizes the semantics of the architectural description level w.r.t. a PPA. The language is intended to be used only as an intermediate description automatically derived from standardized ESL languages such as SystemC when these descriptions are restricted to a mappable subset. Such an intermediate representation is needed to overcome the limitations of SystemC in precisely defining the semantics of the design model and its interfaces as well as to cope with the overwhelming expressive power of SystemC and the large syntactical diversity it allows. With an AML description of the architectural model as a starting point, the paper will show how properties in a standard language like SVA can be automatically generated that guarantee the correctness of the implementation when proven on the design after all refinement steps in the design and the property set have been completed.