Assertion based validation

Assertion based verification

The concept of assertion is very simple . Just state in the program , We say that something must be true , If it's not true , Then the error message can be printed on the screen . stay SystemVerilog In language , Assertions can be made immediately (immediate) And concurrency (concurrent) Two different forms of assertions are used to express . Immediate assertions are very concise , It can be used if、else Wait for a statement to say . Concurrent assertions are very powerful , So this section uses most of the articles to explain how to write concurrent assertions .

stay always This fact can be declared as an immediate assertion in the procedure block ( This assertion is equivalent to a always_comb Process block , But to avoid conceptual confusion , We are only in the integrable RTL Use... In the module always_comb).

always @*
	assert(~(dispense&&ready))
	else $error("dispense and ready both lit!");

The above assertion whenever dispense perhaps ready When the signal changes , Just check if they are both 1. But it is best to detect this condition at the positive jump edge of the clock , Because we are checking a synchronization system . First, write this condition as the following attribute property:

property NotDispenseAndReady;
	@(posedge clock)(~(dispense && ready));
 endproperty

then , As part of concurrent assertions , Test this property , The code is as follows :

assert property(NotDispenseAndReady);

Attribute definitions and assertion declarations can be combined to write . But common programming style suggestions , For the reuse of attributes , It is best to write attribute definitions and assertion declarations in two parts .

Usually , Concurrent assertions