PhD Thesis

< back to PhD thesis

« Automatic synthesis of digital circuits from temporal specifications ».

Author: N. Javaheri
Advisor: D. Borrione
Co-advisor: K. Morin-Allory
President of jury: Ph. Coussy
thesis reviewer(s): P. Prinetto, R. Drechsler,
These de Doctorat Université de Grenoble
Speciality: Nanoélectronique et Nanotechnologies
Defense: October 01 2015
ISBN: 978-2-11-129199-7


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.

pdf pdf