Abstract
We propose a linear complexity approach to achieve automatic synthesis of designs from temporal specifications. It uses concepts from the Assertion-Based Verification. Each property is turned into a component combining classical monitor and generator features: the extended-generator. We connect them with specific components to obtain a design that is correct by construction. It shortens the design flow by removing implementation and functional verification steps. Our approach synthesizes circuits specified by hundreds of temporal properties in a few seconds. Complex examples (i.e. conmax-ip and GenBuf) show the efficiency of the approach.
Chapter PDF
Similar content being viewed by others
Keywords
References
Aziz, A., Balarin, F., Brayton, R.-K., Sangiovanni-Vincentelli, A.-L.: Sequential synthesis using S1S. IEEE Trans. on CAD of Integrated Circuits and Systems 19(10), 1149–1162 (2000)
Anderson, T., Bergeron, J., Cerny, E., Hunter, A., Nightingale, A.: Systemverilog reference verification methodology: Introduction. EE Times, March 27 (2006)
Bloem, R., Cavada, R., Eisner, C., Pill, I., Roveri, M., Semprini, S.: Manual for property simulation and assurance tool (deliverable 1.2/4-5). Technical report, PROSYD Project (January 2004)
Boulé, M., Chenard, J.-S., Zilic, Z.: Adding debug enhancements to assertion checkers for hardware emulation and silicon debug. In: Proceedings of the 24th International Conference on Computer Design, ICCD 2006 (October 2006)
Bloem, R., Galler, S., Jobstman, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science (ENTCS)Â 190 (2007)
Calamé, J.R.: Specification-based test generation with TGV. Technical Report R0508, Centrum voor Wiskunde en Informatica (May 2005)
Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From PSL to NBA: a Modular Symbolic Encoding. In: Proceedings of IEEE Formal Methods for Computer Aided Design, FMCAD 2006, November 11-12, pp. 125–133 (2006)
Cohen, B., Venkataramanan, S., Kumari, A.: Using PSL/Sugar for Formal and Dynamic Verification. VhdlCohen Publishing (2004)
Daniele, M., Giunchiglia, F., Vardi, M.: Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
Foster, H., Krolnik, A., Lacey, D.: Assertion-Based Design. Kluwer Academic Publishers, Dordrecht (2003)
Floyd, R.-W., Ullman, J.D.: The compilation of regular expressions into integrated circuits. J. ACM 29(3), 603–622 (1982)
Foster, H., Wolfshal, Y., Marschner, E., IEEE 1850Â Work Group: IEEE standard for property specification language PSL. pub-IEEE-STD, pub-IEEE-STD:adr (October 2005)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 53. Springer, Heidelberg (2001)
Herveille, R.: WISHBONE system-on-chip (SoC) interconnection architecture for portable IP cores. Technical report (September 2002), http://www.opencores.org/projects.cgi/web/wishbone/wbspec_b3.pdf
Haifa-IBM-Laboratories. RuleBase Parallel Edition. IBM (November 2004)
IBM. PSL/Sugar-based Verification Tools. Web page, http://www.haifa.il.ibm.com/projects/verification/sugar/tools.html
Morin-Allory, K., Borrione, D.: Proven correct monitors from PSL specifications. In: DATE 2006 (January 2006)
Morin-Allory, K., Borrione, D.: On-line monitoring of properties built on regular expressions sequences. In: Vachoux, A. (ed.) Applications of Specification and Design Languages for SoCs. Springer, Heidelberg (2007)
Öberg, J.: ProGram: A Grammar-Based Method for Specification and Hardware Synthesis of Communication Protocols. PhD thesis, Royal Institue of Technologoy - Department of Electronics, Eletronic System Design, Sweden (1999)
Oddos, Y.: PSL Specification for the WISHBONE Interconnect Matrix IP Core (2009), http://tima.imag.fr/vds/horus/synthorus_specs/
Oddos, Y., Morin-Allory, K., Borrione, D.: On-line test vector generation from temporal constraints written in PSL. In: Proc. VLSI SoC 2006 (2006)
PROSYD. Tools and techniques for property verification. Web page, http://www.prosyd.org/twiki/view/Public/DeliverablePageWP3
Seawright, A., Brewer, F.: Clairvoyant: A synthesis system for production-based specification. IEEE Trans. on VLSI, 172–185 (June 1994)
Siegmund, R., Müller, D.: Automatic synthesis of communication controller hardware from protocol specifications. IEEE Design & Test of Computers 19(4), 84–95 (2002)
Srouji, J., Mehta, S., Brophy, D., Pieper, K., Sutherland, S., IEEE 1800Â Work Group: IEEE Standard for SystemVerilog - Unified Hardware Design, Specification, and Verification Language. pub-IEEE-STD, pub-IEEE-STD:adr (November 2005)
Schickel, M., Nimbler, V., Braun, M., Eveking, H.: An Efficient Synthesis Method for Property-Based Design in Formal Verification: On Consistency and Completeness of Property-Sets. In: Advances in Design and Specification Languages for Embedded Systems, pp. 179–196. Springer, Netherlands (2007), 978-1-4020-6149-3
Schickel, M., Oberkönig, M., Schweikert, M., Eveking, H.: A case-study in property-based synthesis: Generating a cache controller from property-set. In: Villar, E. (ed.) Embedded Systems Specification and Design Languages, pp. 271–275. Springer, Netherlands (2008)
Sebastiani, R., Tonetta, S.: More Deterministic vs Smaller Büchi Automata for Efficient LTL Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126–140. Springer, Heidelberg (2003)
Usselman, R.: WISHBONE Interconnect Matrix IP Core (2002), http://www.opencores.org/projects.cgi/web/wb_conmax/overview
Yen, C., Jou, J., Chen, K.: A divide-and-conquer-based algorithm for automatic simulation vector generation. IEEE Design & Test of Computers 21(2), 111–120 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 IFIP International Federation for Information Processing
About this paper
Cite this paper
Oddos, Y., Morin-Allory, K., Borrione, D. (2011). From Assertion-Based Verification to Assertion-Based Synthesis. In: Becker, J., Johann, M., Reis, R. (eds) VLSI-SoC: Technologies for Systems Integration. VLSI-SoC 2009. IFIP Advances in Information and Communication Technology, vol 360. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23120-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-23120-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23119-3
Online ISBN: 978-3-642-23120-9
eBook Packages: Computer ScienceComputer Science (R0)