Name: |
amba_decomposed_lock_4.ref.tlsf |
md5: |
74c52ff5490bdca4891cc73432c075f8 |
FractionOfBinaryClauses |
None |
FractionOfNegativeLiteralsPerClauseEntropy |
None |
FractionOfNegativeLiteralsPerClauseMax |
None |
FractionOfNegativeLiteralsPerClauseMean |
None |
FractionOfNegativeLiteralsPerClauseMin |
None |
FractionOfNegativeLiteralsPerClauseVariationCoefficient |
None |
FractionOfNegativeVariablesEntropy |
None |
FractionOfNegativeVariablesMax |
None |
FractionOfNegativeVariablesMean |
None |
FractionOfNegativeVariablesMin |
None |
FractionOfNegativeVariablesVariationCoefficient |
None |
FractionOfPositiveLiteralsPerClauseEntropy |
None |
FractionOfPositiveLiteralsPerClauseMax |
None |
FractionOfPositiveLiteralsPerClauseMean |
None |
FractionOfPositiveLiteralsPerClauseMin |
None |
FractionOfPositiveLiteralsPerClauseVariationCoefficient |
None |
FractionOfPositiveVariablesEntropy |
None |
FractionOfPositiveVariablesMax |
None |
FractionOfPositiveVariablesMean |
None |
FractionOfPositiveVariablesMin |
None |
FractionOfPositiveVariablesVariationCoefficient |
None |
FractionOfTernaryClauses |
None |
FractionOfUnaryClauses |
None |
ClausesToVariablesRatio |
None |
ClausesToVariablesRatioCubic |
None |
ClausesToVariablesRatioQuadratic |
None |
LinearizedClausesToVariablesRatio |
None |
LinearizedClausesToVariablesRatioQuadratic |
None |
LinearizedClaustesToVariablesRatioCubic |
None |
NumberOfClauses |
None |
NumberOfVariables |
None |
VariablesToClausesRatio |
None |
VariablesToClausesRatioCubic |
None |
VariablesToClausesRatioQuadratic |
None |
ClauseNodeDegreesEntropy |
None |
ClauseNodeDegreesMax |
None |
ClauseNodeDegreesMean |
None |
ClauseNodeDegreesMin |
None |
ClauseNodeDegreesVariationCoefficient |
None |
VariableNodeDegreesEntropy |
None |
VariableNodeDegreesMax |
None |
VariableNodeDegreesMean |
None |
VariableNodeDegreesMin |
None |
VariableNodeDegreesVariationCoefficient |
None |
DegreeEntropy |
None |
DegreeMax |
None |
DegreeMean |
None |
DegreeMin |
None |
DegreeVariationCoefficient |
None |
INFO {
TITLE: "Amba AHB - Decomposed - Lock"
DESCRIPTION: "Lock component of the decomposed Amba AHB Arbiter"
SEMANTICS: Mealy
TARGET: Mealy
}
GLOBAL {
PARAMETERS {
n = 4;
}
DEFINITIONS {
/* Checks whether a bus of size log(n) currently represents
* the numerical value v (encoded in binary).
*/
value(bus,v) = value'(bus,v,0,SIZEOF bus);
value'(bus,v,i,j) =
i >= j : true
bit(v,i) == 1 : value'(bus,v,i + 1,j) && bus[i]
otherwise
... [truncated 1.0 kB]
];
}
OUTPUTS {
LOCKED;
}
ASSUMPTIONS {
// at every time exactely one grant is HIGH
G mutual_exclusion(HGRANT);
G (||[0 <= i < n] HGRANT[i]);
}
INVARIANTS {
// whenever a decicion is taken, the LOCKED signal is updated to
// the HLOCK value of the granted master
&&[0 <= i < n] (DECIDE && X HGRANT[i] -> (X LOCKED <-> X HLOCK[i]));
// otherwise the value is copied
!DECIDE -> (X LOCKED <-> LOCKED)
}
}
//#!SYNTCOMP
//STATUS : realizable
//REF_SIZE : 28
//#.