Skip to Content

SYNTHORUS - Fast Prototyping from Assertions

0
Your rating: None
Tool Name (abbreviation): 
SYNTHORUS
Author(s): 
Dominique Borrion...
(unregistered) Author(s): 
Katell Morin-Allory (Laboratoire TIMA)
Yann Oddos (Syderal)

Assertion-based design is usually understood as specifying the expected properties of a design for verification: observers are produced from the assertions, and the design is verified either statically, by simulation, or online. This was the subject of many previous tools, including our own HORUS. In contrast, with SYNTHORUS [2], we demonstrate the use of assertions to automatically produce a synthesizable HDL model that exhibits the asserted properties. From the assertions, we thus generate the design itself. SYNTHORUS is an extension of HORUS, and takes as input properties written in PSL. The generation method is modular: it is based on the interconnection of elementary library modules for the PSL operators of the property, according to the syntactic structure of the property. The size of the resulting RTL circuit is proportional to the size of the specification. Our method produces RTL designs that are correct by construction: both the library elements and the interconnection procedure are proven correct, using the formal trace semantics of the PSL language, and the PVS theorem prover[1]. The demonstration will show the execution of SYNTHORUS on the specification of a CRC IP. After entering on Byte_nb the frame length, the data bytes are read two at a time on Data, followed by the transmitted CRC. The CRC IP computes it CRC of the input data, and compares the result with the transmitted one. The output signals End and Result indicate if equality has been found at the end of the computation. Fifteen PSL properties are needed for specifying the CRC IP protocol and control part. From these properties, a quick prototype CRC IP is produced. The demonstration will show the design flow from PSL to the resulting net list. We provide a comparison with a golden, hand crafted, CRC circuit. [1] Borrione D., Morin-Allory K., « Proven correct monitors from PSL specifications », Proc. DATE 2006, Munich, Germany, March 2006. [2] Oddos Y., Morin-Allory K., Borrione D., « Synthorus: Highly Efficient Automatic Synthesis from PSL to HDL » , Proc. VLSI-SoC'09, Florianopolis (Brazil), October 2009.

Tag your tool
Keywords: 
Assertion-based design
correct by construction
behavioral property