Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329460 | Electronic Notes in Theoretical Computer Science | 2005 | 16 Pages |
Abstract
This paper formalizes an incremental approach to design flow-control oriented hardware devices described by Moore machines. The method is based on successive additions of new behaviors to a simple device in order to build a more complex one. The new behaviors added must not override the previous ones. A set of CTL formulae is assigned to each step of the design. The links between the formulae of two consecutive design steps are formalized as a set of formula-transformations F, stating that : a CTL formula f is satisfied on a design at step i, iff F(f) is satisfied on the design extended at step i+1. This result has been applied during the design of bus protocol converters in the context on non-regression analysis. It could also be applied in order to simplify both system and formulae in particular cases.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Cécile Braunstein, Emmanuelle Encrenaz,