Sciweavers

ATVA
2009
Springer

Formal Verification for High-Assurance Behavioral Synthesis

13 years 7 months ago
Formal Verification for High-Assurance Behavioral Synthesis
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 emantics. 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.
Sandip Ray, Kecheng Hao, Yan Chen, Fei Xie, Jin Ya
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2009
Where ATVA
Authors Sandip Ray, Kecheng Hao, Yan Chen, Fei Xie, Jin Yang
Comments (0)