PropSYN is property synthesis too, it targets better metrics and verification closure. it is an automatic property generator to enhance coverage-based and assertion-based verification methodologies.


Properties can be operational, microarchitectural or at signal level. Operational properties models input-output properties. They are often protocol specific and span 10s to 100s of clock cycles.


Microarchitectural properties address design implementation and set of hardware functions and their interactions between. They typically span 10s to 100s of clock cycles.


Signal level properties are the easiest to write. They are typically timing invarants and combinatorial.


PropSYN targets microarchitectural level


1)Designers are typically the only ones suited to write accurate properties based on RTL and other design spec intent only available in their heads


2)Designers don’t put high enough priority on adding these to their RTL


At microarchitectural level, can


§Quickly identify verification holes


–Automatic coverage collection on key RTL objects 


–Finds hole in testcases or issues with high random resistance


§Quickly find most of the bugs


–Suitable for regression


–Reusable verification IP


–Assertions closer to bug source




–No reliance on a human designer


–Robust to spec inaccuracies


–An independent method, self-contained


–Detect (currently) unobservable bugs / coverage holes


–Structural properties/covergroups have high coverage of the design

PropSYN runs on RTL microarchitecture and can generate assertions and coverage. It is push-button and requires minimal add-on work. It augments manually developed properties and supports more RTL modeling styles than other formal tools. More importantly, it does not require a stable verification environment such as full regression before getting results. 

PropSYN also generates connectivity properties. Connectivity checks are important because integrating blocks at the system level is challenging. Thousands of pins need to be connected, and this is especially error-prone when third-party Ips are involved. 

PropSYN connectivity checking verifies whether the connections are correct based on user inputs. It checks whether the specified pins are connected, and it also checks the involved conditions and delays. 

PropSYN performs structural connectivity checks and reports problem directly and generates assert properties. This one-step verification can find problems early and simplfies usage.

PropSYN formal proof of connectivity rules can prove if the conditions are satisfiable

如需了解详细产品信息,请联系我们:This email address is being protected from spambots. You need JavaScript enabled to view it. 或者 +86 186 0211 1428