assert_proposition

Ensures that the value of a specified expression is always combinationally TRUE.

Parameters:
severity_level
property_type
msg
coverage_level
Class:
combinational assertion

Syntax 

assert_proposition 

		[#(severity_level, property_type, msg, coverage_level )] 

		instance_name (reset_n, test_expr );

Parameters

 
severity_level
Severity of the failure. Default: ‘OVL_ERROR.
 
property_type
Property type. Default: ‘OVL_ASSERT.
 
msg
Error message printed when assertion fails. Default: “VIOLATION”.
 
coverage_level
Coverage level. Default: ‘OVL_COVER_ALL.

Ports

 
reset_n
 
Active low synchronous reset signal indicating completed initialization.
 
test_expr
 
Expression that should always evaluate to TRUE.

Description

The assert_proposition assertion checker checks the single-bit expression test_expr when it changes value to verify the expression evaluates to TRUE.

Assertion Check

 
ASSERT_PROPOSITION
Expression evaluated to FALSE.

Cover Points

none

Notes

1. Formal verification tools and hardware emulation/acceleration systems might ignore this checker. To verify propositional properties with these tools, consider using assert_always.

See also 

assert_always, assert_always_on_edge, assert_implication, assert_never

Example
assert_proposition #(
 
‘OVL_ERROR,
‘OVL_ASSERT,
“Error: current_addr changed while bus granted”,
‘OVL_COVER_ALL)
// severity_level
// property_type
// msg
// coverage_level
 
valid_current_addr (
 
 
 
bus_gnt,
current_addr == addr );
// reset
// test_expr 
    


 

Ensures that current_addr equals addr while bus_gnt is TRUE.  
    
  
	
  


    
 





 

 




 

 

   
  
    
    © Accellera Organization, Inc. 2005
 All Rights Reserved.
  		
  
    
    Standard OVL V1.1a