The purpose of this article is to provide some basic information about Assertion IP to people who don’t have much information about it.
As per the name, AIP is having assertions written at interface level.
Mostly, AIP is written following strict design coding guidelines so that it can be synthesizable.
AIP can be used in Functional simulation environment as an interface monitor similar to transaction level monitor which is used to check interface behavior as per interface protocol. But, mainly it is targeted for Formal environment with Formal tool.
In Formal environment with Formal tool, it is used to generate stimulus to design, perform interface level checks and provide coverage in the Formal environment to verify the design with very less efforts.
Inside AIP
One will found following details in most of the AIP
- Top level module having Inputs and Outputs which is used to connect [or bind] AIP with DUT
- Parameters to customize AIP to work with customized DUT
- Having interface checkerswritten in the form of properties
- Assert / Assume / Cover declarations of the properties
- Glue logic to help writing complex protocol check conditions in the properties
Bind
Bind will be used to connect AIP with DUT without creating separate test bench module or without editing design code.
One can create separate bind file and using bind keyword, AIP can be connected to DUT.
One can use internal signals and parameters of top level DUT module during binding. Binding AIP with DUT using bind keyword is something like one is creating instance of AIP module inside top level DUT module.
Glue logic
Main purpose of the AIP is to run it with Formal tool in Formal environment. So, AIP should be written in such a way that it will be Formal tool friendly and fully synthesizable. There are various coding guidelines to code AIP to make it formal tool friendly. Those details are out of scope for this article.
Glue logic is required in AIP to avoid writing very complex conditions in the properties. Formal tool will find it very hard to converge on properties if they involve very complex conditions. So, one need to write separate glue logic which can take care of complex condition of the property and code in the property will get simplified.
Assert, Assume and Cover
People familiar with SystemVerilog assertions will be mostly aware of assert, assume and cover declarations of the properties.
AIP will be having various properties to perform protocol checks on given interface.
Then, those properties will be declared as “assert” so that it can indicate adherence or violation of the protocol condition in either formal or simulation environment. In Formal environment, one can look at property falsification and in simulation environment, one can look at failing message in the log.