From Assertion-Based Verification to Assertion-Based Synthesis

摘要

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.