Presentation of SYNTHORUS

SYNTHORUS: Fast Prototyping from Assertions

Correct by construction circuits

Automatic synthesis from temporal specifications consists in automatically transforming a temporal specification into an HDL description which is correct by construction. A great advantage is the elimination of the implementation and functional verification steps from the design flow:

SYNTHORUS automatically synthesizes a temporal specification written in the "simple subset" of PSL (Property Specification Language, IEEE standard 1850) into a correct by construction HDL description. It uses Assertion-Based Verification and turns assertions and assumptions into components mixing monitors and generators: the extended-generators. They are the basic components of the synthesized design and have been proved correct with respect to the PSL semantics. Combined with specific components called Solvers, the resulting circuit provides the final design corresponding to a given specification.

Instead of using an automata based approach or restricting the application to a specific type of designs, SYNTHORUS uses a modular construction inspired from the HORUS technology. The complexity is then encapsulated in different levels of basic components. The synthesis method generates circuits that comply with the PSL semantics. Experiments on some control-dominated systems showed that a system described as a dozen of PSL properties directly extracted from its specification was generated as around 3500 lines of correct-by-construction RTL.

References

Y.Oddos, K.Morin-Allory, D.Borrione: "On-line vector generation from temporal constraints written in PSL". Proc. VLSI-SoC'2006, October 2006.
Y.Oddos, K.Morin-Allory, D.Borrione: "Assertion-Based Design with Horus". Proc. MEMOCODE'2008, June 2008 (short paper).
Y.Oddos, K.Morin-Allory, D.Borrione: "Synthorus: Highly Efficient Automatic Synthesis from PSL to HDL". Proc. IFIP/IEEE International Conference On Very Large Scale Integration (VLSI-SoC'09), Florianopolis (Brazil), October 2009.
Y.Oddos: "Vérification semi-formelle et synthèse automatique de circuits à partir de spécifications temporelles écrites en PSL". PhD Thesis, Grenoble University, November 2009 (in French).