Formal Verification for High-Assurance Behavioral Synthesis

S. Ray, K. Hao, Y. Chen, F. Xie, and J. Yang. In Z. Liu and A. P. Ravn, editors, Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA 2009), Macao SAR, China, October 2009, volume 5799 of LNCS, pages 337-351. Springer.

© Springer-Verlag Berlin Heidelberg 2009.

Abstract

We present a framework for certifying hardware designs generated through behavioral synthesis, by using formal verification to certify the associated synthesis transformations. We show how to decompose this certification into two components, which can be respectively handled by the complementary verification techniques, theorem proving and model checking. The approach produces a certified reference flow, composed of transformations distilled from production synthesis tools but represented as transformations on graphs with an associated formal semantics. This tool-independent abstraction disentangles our framework from the inner workings of specific synthesis tools while permitting certification of hardware designs generated from a broad class of behavioral descriptions. We provide experimental results suggesting the scalability on practical designs.

Relevant files

Paper (ps, pdf)

BibTex

@Inproceedings{ray-formal,
  author    = "S. Ray and K. Hao and F. Xie and J. Yang",
  title     = "{Formal Verification for High-Assurance Behavioral Synthesis}",
  booktitle = "{Proceedings of the 7th International Symposium on Automated 
                Technology for Verification and Analysis (ATVA 2009)}",
  editor    = "Z. Liu and A. P. Ravn",
  address   = "{Macao SAR, China}",
  month     = oct,
  year      = "2009",
  series    = "LNCS",
  volume    = "5799",
  pages     = "337-351",
  publisher = "Springer"
}