Top level design units: formal_request_grant_properties { "hardwareDesign": { "instances": [ {"instance": "dut", "module": "request_grant_fsm"} ] }, "hostDesign": { "instances": [ {"instance": "formal_request_grant_properties", "module": "formal_request_grant_properties"} ] }, "bindings": [ {"host": "formal_request_grant_properties", "instance": "dut", "hardwareModule": "request_grant_fsm"} ], "formalDesign": { "modules": [ {"module": "request_grant_fsm", "directives": []}, {"module": "formal_request_grant_properties", "directives": [{"name": "request_grant_contract", "kind": "assert", "clock": "clk"}]} ] }, "semanticTree": { "design":{ "name":"$root", "kind":"Root", "addr":2199035517696, "members":[ { "name":"", "kind":"CompilationUnit", "addr":2199035395440 }, { "name":"", "kind":"CompilationUnit", "addr":2199035395808 }, { "name":"formal_request_grant_properties", "kind":"Instance", "source_file":"properties\/request_grant_properties.sv", "source_line":1, "source_column":8, "addr":2199035397888, "body":{ "name":"formal_request_grant_properties", "kind":"InstanceBody", "source_file":"properties\/request_grant_properties.sv", "source_line":1, "source_column":8, "addr":2199035396176, "members":[ { "name":"clk", "kind":"Variable", "source_file":"properties\/request_grant_properties.sv", "source_line":2, "source_column":11, "addr":2199035396368, "type":"logic", "lifetime":"Static" }, { "name":"rst_n", "kind":"Variable", "source_file":"properties\/request_grant_properties.sv", "source_line":3, "source_column":11, "addr":2199035396536, "type":"logic", "lifetime":"Static" }, { "name":"request", "kind":"Variable", "source_file":"properties\/request_grant_properties.sv", "source_line":4, "source_column":11, "addr":2199035396704, "type":"logic", "lifetime":"Static" }, { "name":"ready", "kind":"Variable", "source_file":"properties\/request_grant_properties.sv", "source_line":5, "source_column":11, "addr":2199035396872, "type":"logic", "lifetime":"Static" }, { "name":"busy", "kind":"Variable", "source_file":"properties\/request_grant_properties.sv", "source_line":6, "source_column":11, "addr":2199035397040, "type":"logic", "lifetime":"Static" }, { "name":"grant", "kind":"Variable", "source_file":"properties\/request_grant_properties.sv", "source_line":7, "source_column":11, "addr":2199035397208, "type":"logic", "lifetime":"Static" }, { "name":"dut", "kind":"Instance", "source_file":"properties\/request_grant_properties.sv", "source_line":9, "source_column":23, "addr":2199035398040, "body":{ "name":"request_grant_fsm", "kind":"InstanceBody", "source_file":"rtl\/request_grant_fsm.sv", "source_line":1, "source_column":8, "addr":2199035398184, "members":[ { "name":"clk", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":2, "source_column":18, "addr":2199035406736, "type":"logic", "direction":"In", "internalSymbol":"2199035406904 clk" }, { "name":"clk", "kind":"Net", "source_file":"rtl\/request_grant_fsm.sv", "source_line":2, "source_column":18, "addr":2199035406904, "type":"logic", "netType":{ "name":"wire", "kind":"NetType", "addr":2199035515008, "type":"logic" } }, { "name":"rst_n", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":3, "source_column":18, "addr":2199035407096, "type":"logic", "direction":"In", "internalSymbol":"2199035407264 rst_n" }, { "name":"rst_n", "kind":"Net", "source_file":"rtl\/request_grant_fsm.sv", "source_line":3, "source_column":18, "addr":2199035407264, "type":"logic", "netType":{ "name":"wire", "kind":"NetType", "addr":2199035515008, "type":"logic" } }, { "name":"request", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":4, "source_column":18, "addr":2199035407456, "type":"logic", "direction":"In", "internalSymbol":"2199035407624 request" }, { "name":"request", "kind":"Net", "source_file":"rtl\/request_grant_fsm.sv", "source_line":4, "source_column":18, "addr":2199035407624, "type":"logic", "netType":{ "name":"wire", "kind":"NetType", "addr":2199035515008, "type":"logic" } }, { "name":"ready", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":5, "source_column":18, "addr":2199035407816, "type":"logic", "direction":"Out", "internalSymbol":"2199035407984 ready" }, { "name":"ready", "kind":"Variable", "source_file":"rtl\/request_grant_fsm.sv", "source_line":5, "source_column":18, "addr":2199035407984, "type":"logic", "lifetime":"Static" }, { "name":"busy", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":6, "source_column":18, "addr":2199035408152, "type":"logic", "direction":"Out", "internalSymbol":"2199035408320 busy" }, { "name":"busy", "kind":"Variable", "source_file":"rtl\/request_grant_fsm.sv", "source_line":6, "source_column":18, "addr":2199035408320, "type":"logic", "lifetime":"Static" }, { "name":"grant", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":7, "source_column":18, "addr":2199035408488, "type":"logic", "direction":"Out", "internalSymbol":"2199035408656 grant" }, { "name":"grant", "kind":"Variable", "source_file":"rtl\/request_grant_fsm.sv", "source_line":7, "source_column":18, "addr":2199035408656, "type":"logic", "lifetime":"Static" }, { "name":"state_t", "kind":"EnumType", "source_file":"rtl\/request_grant_fsm.sv", "source_line":9, "source_column":13, "addr":2199035405640, "members":[ { "name":"idle", "kind":"EnumValue", "source_file":"rtl\/request_grant_fsm.sv", "source_line":10, "source_column":9, "addr":2199035405800, "value":"2'b0" }, { "name":"queued", "kind":"EnumValue", "source_file":"rtl\/request_grant_fsm.sv", "source_line":11, "source_column":9, "addr":2199035406056, "value":"2'b1" }, { "name":"granting", "kind":"EnumValue", "source_file":"rtl\/request_grant_fsm.sv", "source_line":12, "source_column":9, "addr":2199035406312, "value":"2'b10" } ], "baseType":"logic[1:0]" }, { "name":"state_t", "kind":"TypeAlias", "source_file":"rtl\/request_grant_fsm.sv", "source_line":13, "source_column":7, "addr":2199035398536, "target":"2199035405640 request_grant_fsm.state_t" }, { "name":"state", "kind":"Variable", "source_file":"rtl\/request_grant_fsm.sv", "source_line":15, "source_column":13, "addr":2199035406568, "type":"2199035398536 request_grant_fsm.state_t", "lifetime":"Static" }, { "name":"", "kind":"ProceduralBlock", "source_file":"rtl\/request_grant_fsm.sv", "source_line":17, "source_column":5, "addr":2199035398792, "procedureKind":"AlwaysFF", "body":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":17, "source_line_end":28, "source_column_start":15, "source_column_end":8, "kind":"Timed", "timing":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":17, "source_line_end":17, "source_column_start":17, "source_column_end":28, "kind":"SignalEvent", "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":17, "source_line_end":17, "source_column_start":25, "source_column_end":28, "kind":"NamedValue", "type":"logic", "symbol":"2199035406904 clk" }, "edge":"PosEdge" }, "stmt":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":18, "source_line_end":27, "source_column_start":9, "source_column_end":12, "kind":"Block", "blockKind":"Sequential", "body":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":18, "source_line_end":27, "source_column_start":9, "source_column_end":12, "kind":"Conditional", "conditions":[ { "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":18, "source_line_end":18, "source_column_start":13, "source_column_end":19, "kind":"UnaryOp", "type":"logic", "op":"LogicalNot", "operand":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":18, "source_line_end":18, "source_column_start":14, "source_column_end":19, "kind":"NamedValue", "type":"logic", "symbol":"2199035407264 rst_n" } } } ], "check":"None", "ifTrue":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":19, "source_line_end":19, "source_column_start":13, "source_column_end":27, "kind":"ExpressionStatement", "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":19, "source_line_end":19, "source_column_start":13, "source_column_end":26, "kind":"Assignment", "type":"2199035398536 request_grant_fsm.state_t", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":19, "source_line_end":19, "source_column_start":13, "source_column_end":18, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":19, "source_line_end":19, "source_column_start":22, "source_column_end":26, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035405800 idle", "constant":"2'b0" }, "isNonBlocking":true } }, "ifFalse":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":21, "source_line_end":26, "source_column_start":13, "source_column_end":20, "kind":"Block", "blockKind":"Sequential", "body":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":21, "source_line_end":26, "source_column_start":13, "source_column_end":20, "kind":"Case", "condition":"Normal", "check":"Unique", "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":21, "source_line_end":21, "source_column_start":26, "source_column_end":31, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "items":[ { "expressions":[ { "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":13, "source_column_end":17, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035405800 idle", "constant":"2'b0" } ], "stmt":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":23, "source_column_end":56, "kind":"ExpressionStatement", "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":23, "source_column_end":55, "kind":"Assignment", "type":"2199035398536 request_grant_fsm.state_t", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":23, "source_column_end":28, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":32, "source_column_end":55, "kind":"ConditionalOp", "type":"2199035405640 request_grant_fsm.state_t", "conditions":[ { "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":32, "source_column_end":39, "kind":"NamedValue", "type":"logic", "symbol":"2199035407624 request" } } ], "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":42, "source_column_end":48, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035406056 queued", "constant":"2'b1" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":22, "source_line_end":22, "source_column_start":51, "source_column_end":55, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035405800 idle", "constant":"2'b0" } }, "isNonBlocking":true } } }, { "expressions":[ { "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":23, "source_line_end":23, "source_column_start":13, "source_column_end":19, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035406056 queued", "constant":"2'b1" } ], "stmt":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":23, "source_line_end":23, "source_column_start":23, "source_column_end":41, "kind":"ExpressionStatement", "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":23, "source_line_end":23, "source_column_start":23, "source_column_end":40, "kind":"Assignment", "type":"2199035398536 request_grant_fsm.state_t", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":23, "source_line_end":23, "source_column_start":23, "source_column_end":28, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":23, "source_line_end":23, "source_column_start":32, "source_column_end":40, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035406312 granting", "constant":"2'b10" }, "isNonBlocking":true } } }, { "expressions":[ { "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":24, "source_line_end":24, "source_column_start":13, "source_column_end":21, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035406312 granting", "constant":"2'b10" } ], "stmt":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":24, "source_line_end":24, "source_column_start":23, "source_column_end":37, "kind":"ExpressionStatement", "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":24, "source_line_end":24, "source_column_start":23, "source_column_end":36, "kind":"Assignment", "type":"2199035398536 request_grant_fsm.state_t", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":24, "source_line_end":24, "source_column_start":23, "source_column_end":28, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":24, "source_line_end":24, "source_column_start":32, "source_column_end":36, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035405800 idle", "constant":"2'b0" }, "isNonBlocking":true } } } ], "defaultCase":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":25, "source_line_end":25, "source_column_start":23, "source_column_end":37, "kind":"ExpressionStatement", "expr":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":25, "source_line_end":25, "source_column_start":23, "source_column_end":36, "kind":"Assignment", "type":"2199035398536 request_grant_fsm.state_t", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":25, "source_line_end":25, "source_column_start":23, "source_column_end":28, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":25, "source_line_end":25, "source_column_start":32, "source_column_end":36, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035405800 idle", "constant":"2'b0" }, "isNonBlocking":true } } } } } } } }, { "name":"", "kind":"ContinuousAssign", "source_file":"rtl\/request_grant_fsm.sv", "source_line":35, "source_column":12, "addr":2199035408872, "assignment":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":35, "source_line_end":35, "source_column_start":12, "source_column_end":33, "kind":"Assignment", "type":"logic", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":35, "source_line_end":35, "source_column_start":12, "source_column_end":17, "kind":"NamedValue", "type":"logic", "symbol":"2199035407984 ready" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":35, "source_line_end":35, "source_column_start":20, "source_column_end":33, "kind":"BinaryOp", "type":"logic", "op":"Equality", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":35, "source_line_end":35, "source_column_start":20, "source_column_end":25, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":35, "source_line_end":35, "source_column_start":29, "source_column_end":33, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035405800 idle", "constant":"2'b0" } }, "isNonBlocking":false } }, { "name":"", "kind":"ContinuousAssign", "source_file":"rtl\/request_grant_fsm.sv", "source_line":37, "source_column":12, "addr":2199035408968, "assignment":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":37, "source_line_end":37, "source_column_start":12, "source_column_end":33, "kind":"Assignment", "type":"logic", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":37, "source_line_end":37, "source_column_start":12, "source_column_end":16, "kind":"NamedValue", "type":"logic", "symbol":"2199035408320 busy" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":37, "source_line_end":37, "source_column_start":20, "source_column_end":33, "kind":"BinaryOp", "type":"logic", "op":"Inequality", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":37, "source_line_end":37, "source_column_start":20, "source_column_end":25, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":37, "source_line_end":37, "source_column_start":29, "source_column_end":33, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035405800 idle", "constant":"2'b0" } }, "isNonBlocking":false } }, { "name":"", "kind":"ContinuousAssign", "source_file":"rtl\/request_grant_fsm.sv", "source_line":38, "source_column":12, "addr":2199035409064, "assignment":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":38, "source_line_end":38, "source_column_start":12, "source_column_end":37, "kind":"Assignment", "type":"logic", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":38, "source_line_end":38, "source_column_start":12, "source_column_end":17, "kind":"NamedValue", "type":"logic", "symbol":"2199035408656 grant" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":38, "source_line_end":38, "source_column_start":20, "source_column_end":37, "kind":"BinaryOp", "type":"logic", "op":"Equality", "left":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":38, "source_line_end":38, "source_column_start":20, "source_column_end":25, "kind":"NamedValue", "type":"2199035398536 request_grant_fsm.state_t", "symbol":"2199035406568 state" }, "right":{ "source_file_start":"rtl\/request_grant_fsm.sv", "source_file_end":"rtl\/request_grant_fsm.sv", "source_line_start":38, "source_line_end":38, "source_column_start":29, "source_column_end":37, "kind":"NamedValue", "type":"2199035405640 request_grant_fsm.state_t", "symbol":"2199035406312 granting", "constant":"2'b10" } }, "isNonBlocking":false } } ], "definition":"2199036755968 request_grant_fsm" }, "connections":[ { "port":{ "name":"clk", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":2, "source_column":18, "addr":2199035406736, "type":"logic", "direction":"In", "internalSymbol":"2199035406904 clk" }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":10, "source_line_end":10, "source_column_start":10, "source_column_end":13, "kind":"NamedValue", "type":"logic", "symbol":"2199035396368 clk" } }, { "port":{ "name":"rst_n", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":3, "source_column":18, "addr":2199035407096, "type":"logic", "direction":"In", "internalSymbol":"2199035407264 rst_n" }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":11, "source_line_end":11, "source_column_start":10, "source_column_end":15, "kind":"NamedValue", "type":"logic", "symbol":"2199035396536 rst_n" } }, { "port":{ "name":"request", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":4, "source_column":18, "addr":2199035407456, "type":"logic", "direction":"In", "internalSymbol":"2199035407624 request" }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":12, "source_line_end":12, "source_column_start":10, "source_column_end":17, "kind":"NamedValue", "type":"logic", "symbol":"2199035396704 request" } }, { "port":{ "name":"ready", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":5, "source_column":18, "addr":2199035407816, "type":"logic", "direction":"Out", "internalSymbol":"2199035407984 ready" }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":13, "source_line_end":13, "source_column_start":10, "source_column_end":15, "kind":"Assignment", "type":"logic", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":13, "source_line_end":13, "source_column_start":10, "source_column_end":15, "kind":"NamedValue", "type":"logic", "symbol":"2199035396872 ready" }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":13, "source_line_end":13, "source_column_start":10, "source_column_end":15, "kind":"EmptyArgument", "type":"logic" }, "isNonBlocking":false } }, { "port":{ "name":"busy", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":6, "source_column":18, "addr":2199035408152, "type":"logic", "direction":"Out", "internalSymbol":"2199035408320 busy" }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":14, "source_line_end":14, "source_column_start":10, "source_column_end":14, "kind":"Assignment", "type":"logic", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":14, "source_line_end":14, "source_column_start":10, "source_column_end":14, "kind":"NamedValue", "type":"logic", "symbol":"2199035397040 busy" }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":14, "source_line_end":14, "source_column_start":10, "source_column_end":14, "kind":"EmptyArgument", "type":"logic" }, "isNonBlocking":false } }, { "port":{ "name":"grant", "kind":"Port", "source_file":"rtl\/request_grant_fsm.sv", "source_line":7, "source_column":18, "addr":2199035408488, "type":"logic", "direction":"Out", "internalSymbol":"2199035408656 grant" }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":15, "source_line_end":15, "source_column_start":10, "source_column_end":15, "kind":"Assignment", "type":"logic", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":15, "source_line_end":15, "source_column_start":10, "source_column_end":15, "kind":"NamedValue", "type":"logic", "symbol":"2199035397208 grant" }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":15, "source_line_end":15, "source_column_start":10, "source_column_end":15, "kind":"EmptyArgument", "type":"logic" }, "isNonBlocking":false } } ] }, { "name":"request_grant_contract", "kind":"Property", "source_file":"properties\/request_grant_properties.sv", "source_line":18, "source_column":14, "addr":2199035397456 }, { "name":"request_grant_contract_assert", "kind":"StatementBlock", "source_file":"properties\/request_grant_properties.sv", "source_line":25, "source_column":5, "addr":2199035397720 }, { "name":"", "kind":"ProceduralBlock", "source_file":"properties\/request_grant_properties.sv", "source_line":25, "source_column":5, "addr":2199035397600, "procedureKind":"Always", "body":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":25, "source_line_end":26, "source_column_start":5, "source_column_end":50, "kind":"Block", "blockKind":"Sequential", "block":"2199035397720 request_grant_contract_assert", "body":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":25, "source_line_end":26, "source_column_start":5, "source_column_end":50, "kind":"ConcurrentAssertion", "propertySpec":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":26, "source_line_end":26, "source_column_start":26, "source_column_end":48, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":26, "source_line_end":26, "source_column_start":26, "source_column_end":48, "kind":"AssertionInstance", "type":"property", "symbol":"2199035397456 request_grant_contract", "body":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":19, "source_line_end":22, "source_column_start":9, "source_column_end":66, "kind":"Clocking", "clocking":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":19, "source_line_end":19, "source_column_start":11, "source_column_end":22, "kind":"SignalEvent", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":19, "source_line_end":19, "source_column_start":19, "source_column_end":22, "kind":"NamedValue", "type":"logic", "symbol":"2199035396368 clk" }, "edge":"PosEdge" }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":19, "source_line_end":19, "source_column_start":24, "source_column_end":44, "kind":"DisableIff", "condition":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":19, "source_line_end":19, "source_column_start":37, "source_column_end":43, "kind":"UnaryOp", "type":"logic", "op":"LogicalNot", "operand":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":19, "source_line_end":19, "source_column_start":38, "source_column_end":43, "kind":"NamedValue", "type":"logic", "symbol":"2199035396536 rst_n" } }, "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":22, "source_column_start":9, "source_column_end":66, "kind":"Binary", "op":"And", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":21, "source_column_start":9, "source_column_end":51, "kind":"Binary", "op":"And", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":20, "source_column_start":9, "source_column_end":35, "kind":"Unary", "op":"Always", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":20, "source_column_start":17, "source_column_end":34, "kind":"Binary", "op":"Iff", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":20, "source_column_start":18, "source_column_end":22, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":20, "source_column_start":18, "source_column_end":22, "kind":"NamedValue", "type":"logic", "symbol":"2199035397040 busy" } }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":20, "source_column_start":27, "source_column_end":33, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":20, "source_column_start":27, "source_column_end":33, "kind":"UnaryOp", "type":"logic", "op":"LogicalNot", "operand":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":20, "source_line_end":20, "source_column_start":28, "source_column_end":33, "kind":"NamedValue", "type":"logic", "symbol":"2199035396872 ready" } } } } }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":9, "source_column_end":51, "kind":"Unary", "op":"Always", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":17, "source_column_end":50, "kind":"Binary", "op":"Implies", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":18, "source_column_end":23, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":18, "source_column_end":23, "kind":"NamedValue", "type":"logic", "symbol":"2199035397208 grant" } }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":32, "source_column_end":49, "kind":"Binary", "op":"And", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":33, "source_column_end":37, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":33, "source_column_end":37, "kind":"NamedValue", "type":"logic", "symbol":"2199035397040 busy" } }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":42, "source_column_end":48, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":42, "source_column_end":48, "kind":"UnaryOp", "type":"logic", "op":"LogicalNot", "operand":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":21, "source_line_end":21, "source_column_start":43, "source_column_end":48, "kind":"NamedValue", "type":"logic", "symbol":"2199035396872 ready" } } } } } } }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":9, "source_column_end":66, "kind":"Unary", "op":"Always", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":17, "source_column_end":65, "kind":"Binary", "op":"Implies", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":18, "source_column_end":37, "kind":"Binary", "op":"And", "left":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":19, "source_column_end":26, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":19, "source_column_end":26, "kind":"NamedValue", "type":"logic", "symbol":"2199035396704 request" } }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":31, "source_column_end":36, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":31, "source_column_end":36, "kind":"NamedValue", "type":"logic", "symbol":"2199035396872 ready" } } }, "right":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":46, "source_column_end":64, "kind":"Unary", "op":"SEventually", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":59, "source_column_end":64, "kind":"Simple", "expr":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":22, "source_line_end":22, "source_column_start":59, "source_column_end":64, "kind":"NamedValue", "type":"logic", "symbol":"2199035397208 grant" } } } } } } } }, "isRecursiveProperty":false, "localVars":[] } }, "ifTrue":{ "source_file_start":"properties\/request_grant_properties.sv", "source_file_end":"properties\/request_grant_properties.sv", "source_line_start":26, "source_line_end":26, "source_column_start":49, "source_column_end":50, "kind":"Empty" }, "assertionKind":"Assert" } } } ], "definition":"2199036756864 formal_request_grant_properties" }, "connections":[] } ] } } }