< retour aux séminaires

Negin JAVAHERI, Laboratoire TIMA - Equipe AMfoRS,

Theme: Synthèse automatique de circuits numériques à partir de spécifications temporelles
Date: Vendredi 16 octobre 2015 à 14 h 00, Laboratoire TIMA - Salle T312


The work presented in this thesis aims at automatically prototype communication and control designs from declarative temporal specifications. From a set of PSL1 properties, we produce a synthesizable RTL design automatically. The proposed method is modular, in contrast to previously published methods that were based on automata theory. From each property, we produce a component that observes some operands and generates waveforms for the other operands: the reactant. First, a library of primitive reactants has been provided for FL2 and SERE3 operators. To this goal, a dependency relation is defined for each operator that expresses the dependency among its operands using the operator's semantics. Then, the dependency relation of each operator is interpreted as a hardware component that implements the operator : the operator's primitive reactant. Using this formalization, a method is proposed to automatically decide which signals of a property are observed and which are generated. In the cases when specifying the signal direction is not possible, a solver is implemented to identify the signal value. In addition, the way of identifying the value of the signal that is generated in several properties is addressed. The final circuit is the interconnection of the properties' reactants and solvers. A prototype tool SyntHorus2, which is an extension to HORUS, has been developed. It takes PSL properties as its inputs, and generates the synthesizable VHDL code of the circuit. In addition, it generates some complementary properties to verify if the set of specification is coherent and complete. The method is efficient, and synthesizes control circuits in a few seconds. Results obtained on classical benchmarks show that our technique compiles properties more efficiently than previous prototype tools.
Keywords: PSL, assertion-based design, reactant, automatic synthesis, dependency graph, annotation, resolution, solver.