Skip to content

Commit

Permalink
Implement PSL logical operators. Issue #998
Browse files Browse the repository at this point in the history
  • Loading branch information
@nickg
nickg committed Nov 3, 2024
1 parent c16d2ae commit ef8cfd0
Show file tree
Hide file tree
Showing 10 changed files with 190 additions and 76 deletions.
115 changes: 83 additions & 32 deletions src/parse.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2411,11 +2411,11 @@ static void declare_generic_ops(tree_t parent, type_t type)
static bool is_vhdl_infix_op(token_t tok)
{
return tok == tEQ || tok == tNEQ || tok == tLT || tok == tGT
|| tok == tLE || tok == tGE || tok == tAND || tok == tOR || tok == tNAND
|| tok == tNOR || tok == tXOR || tok == tXNOR || tok == tMOD
|| tok == tREM || tok == tPLUS || tok == tMINUS || tok == tTIMES
|| tok == tOVER || tok == tPOWER || tok == tMEQ || tok == tMNEQ
|| tok == tMLT || tok == tMLE || tok == tMGT || tok == tMGE;
|| tok == tLE || tok == tGE || tok == tNAND || tok == tNOR
|| tok == tXOR || tok == tXNOR || tok == tMOD || tok == tREM
|| tok == tPLUS || tok == tMINUS || tok == tTIMES || tok == tOVER
|| tok == tPOWER || tok == tMEQ || tok == tMNEQ || tok == tMLT
|| tok == tMLE || tok == tMGT || tok == tMGE;
}

static void add_predef_alias(tree_t t, void *context)
Expand Down Expand Up @@ -4919,22 +4919,10 @@ static tree_t p_expression_with_head(tree_t head)
int loop_limit = (scan(tNOR, tNAND) ? 1 : INT_MAX);

while (loop_limit-- && scan(tAND, tOR, tXOR, tNAND, tNOR, tXNOR)) {
ident_t op;
switch (one_of(tAND, tOR, tXOR, tNAND, tNOR, tXNOR)) {
case tAND: op = well_known(W_OP_AND); break;
case tOR: op = well_known(W_OP_OR); break;
case tXOR: op = well_known(W_OP_XOR); break;
case tNAND: op = well_known(W_OP_NAND); break;
case tNOR: op = well_known(W_OP_NOR); break;
case tXNOR: op = well_known(W_OP_XNOR); break;
default: op = error_marker();
}

tree_t left = expr;

expr = tree_new(T_FCALL);
tree_set_ident(expr, op);
binary_op(expr, left, p_relation);
tree_t new = tree_new(T_FCALL);
tree_set_ident(new, p_logical_operator());
binary_op(new, expr, p_relation);
expr = new;
}

return expr;
Expand Down Expand Up @@ -11365,7 +11353,17 @@ static psl_node_t p_psl_or_hdl_expression(void)

BEGIN("PSL or HDL expression");

tree_t expr = p_expression();
tree_t expr = p_relation(NULL);

int loop_limit = (scan(tNOR, tNAND) ? 1 : INT_MAX);

// AND and OR must be parsed as PSL operators
while (loop_limit-- && scan(tXOR, tNAND, tNOR, tXNOR)) {
tree_t new = tree_new(T_FCALL);
tree_set_ident(new, p_logical_operator());
binary_op(new, expr, p_relation);
expr = new;
}

psl_node_t p = psl_new(P_HDL_EXPR);
psl_set_tree(p, expr);
Expand Down Expand Up @@ -12028,7 +12026,12 @@ static psl_node_t p_psl_sequence(void)
break;
}

p = p_psl_or_hdl_expression();
tree_t expr = p_expression();

p = psl_new(P_HDL_EXPR);
psl_set_tree(p, expr);
psl_set_loc(p, tree_loc(expr));
psl_set_type(p, PSL_TYPE_BOOLEAN);

// [= and [-> are only allowed after boolean -> no need to recurse
// or create new SERE
Expand Down Expand Up @@ -12077,6 +12080,8 @@ static psl_node_t p_psl_fl_property(void)
// | next_event! ( Boolean ) [ Number ] ( FL_Property )
// | FL_Property -> FL_Property
// | FL_Property <-> FL_Property
// | FL_Property or FL_Property
// | FL_Property and FL_Property
// | FL_Property until! FL_Property
// | FL_Property until!_ FL_Property
// | FL_Property until FL_Property
Expand All @@ -12099,6 +12104,7 @@ static psl_node_t p_psl_fl_property(void)

p = psl_new(P_ALWAYS);
psl_set_value(p, p_psl_fl_property());
psl_set_loc(p, CURRENT_LOC);
}
break;

Expand All @@ -12108,6 +12114,7 @@ static psl_node_t p_psl_fl_property(void)

p = psl_new(P_NEVER);
psl_set_value(p, p_psl_fl_property());
psl_set_loc(p, CURRENT_LOC);
}
break;

Expand All @@ -12117,6 +12124,7 @@ static psl_node_t p_psl_fl_property(void)

p = psl_new(P_EVENTUALLY);
psl_set_value(p, p_psl_fl_property());
psl_set_loc(p, CURRENT_LOC);
}
break;

Expand All @@ -12143,6 +12151,7 @@ static psl_node_t p_psl_fl_property(void)
}

psl_set_value(p, p_psl_fl_property());
psl_set_loc(p, CURRENT_LOC);
}
break;

Expand All @@ -12163,6 +12172,7 @@ static psl_node_t p_psl_fl_property(void)
consume(tRSQUARE);

psl_set_value(p, p_psl_fl_property());
psl_set_loc(p, CURRENT_LOC);
}
break;

Expand All @@ -12183,6 +12193,7 @@ static psl_node_t p_psl_fl_property(void)
consume(tRSQUARE);

psl_set_value(p, p_psl_fl_property());
psl_set_loc(p, CURRENT_LOC);
}
break;

Expand Down Expand Up @@ -12215,6 +12226,8 @@ static psl_node_t p_psl_fl_property(void)
consume(tLPAREN);
psl_set_value(p, p_psl_fl_property());
consume(tRPAREN);

psl_set_loc(p, CURRENT_LOC);
}
break;

Expand All @@ -12231,30 +12244,68 @@ static psl_node_t p_psl_fl_property(void)
tree_t expr = p_expression_with_head(psl_tree(p));
psl_set_tree(p, expr);
}

psl_set_loc(p, CURRENT_LOC);
}
break;

default:
case tLBRACE:
p = p_psl_sequence();
break;
}

psl_set_loc(p, CURRENT_LOC);
default:
p = p_psl_or_hdl_expression();
break;
}

const token_t infix = peek();
switch (infix) {
case tIFIMPL:
case tIFFIMPL:
case tAND:
case tOR:
{
consume(infix);

psl_node_t impl = psl_new(P_IMPLICATION);
psl_set_subkind(impl, infix == tIFIMPL ? PSL_IMPL_IF : PSL_IMPL_IFF);
psl_add_operand(impl, p);
psl_add_operand(impl, p_psl_fl_property());
psl_set_loc(impl, CURRENT_LOC);
psl_logic_t kind;
switch (infix) {
case tAND: kind = PSL_LOGIC_AND; break;
case tOR: kind = PSL_LOGIC_OR; break;
case tIFIMPL: kind = PSL_LOGIC_IF; break;
case tIFFIMPL: kind = PSL_LOGIC_IFF; break;
default: should_not_reach_here();
}

return impl;
psl_node_t right = p_psl_fl_property();

// A logical operation where the two operands are HDL
// expressions should be parsed as a single HDL expression
const bool prefer_hdl =
(kind == PSL_LOGIC_OR || kind == PSL_LOGIC_AND)
&& psl_kind(p) == P_HDL_EXPR && psl_kind(right) == P_HDL_EXPR;

if (prefer_hdl) {
ident_t op = well_known(kind == PSL_LOGIC_OR ? W_OP_OR : W_OP_AND);

tree_t fcall = tree_new(T_FCALL);
tree_set_ident(fcall, op);
tree_set_loc(fcall, CURRENT_LOC);
add_param(fcall, psl_tree(p), P_POS, NULL);
add_param(fcall, psl_tree(right), P_POS, NULL);

psl_set_tree(p, fcall);
psl_set_loc(p, CURRENT_LOC);
return p;
}
else {
psl_node_t log = psl_new(P_LOGICAL);
psl_set_subkind(log, kind);
psl_add_operand(log, p);
psl_add_operand(log, right);
psl_set_loc(log, CURRENT_LOC);

return log;
}
}

case tSUFFIXOVR:
Expand Down
10 changes: 6 additions & 4 deletions src/psl/psl-dump.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,10 +82,12 @@ static void psl_dump_never(psl_node_t p)
psl_dump(psl_value(p));
}

static void psl_dump_implication(psl_node_t p)
static void psl_dump_logical(psl_node_t p)
{
static const char *map[] = { "->", "<->", "and", "or" };

psl_dump(psl_operand(p, 0));
print_syntax(" -> (");
print_syntax(" %s (", map[psl_subkind(p)]);
psl_dump(psl_operand(p, 1));
print_syntax(")");
}
Expand Down Expand Up @@ -222,8 +224,8 @@ void psl_dump(psl_node_t p)
case P_HDL_EXPR:
vhdl_dump(psl_tree(p), 0);
break;
case P_IMPLICATION:
psl_dump_implication(p);
case P_LOGICAL:
psl_dump_logical(p);
break;
case P_NEXT:
psl_dump_next(p);
Expand Down
81 changes: 57 additions & 24 deletions src/psl/psl-fsm.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,30 +114,56 @@ static void connect_default(fsm_state_t *from, fsm_state_t *to,
add_edge(from, to, EDGE_NEXT, NULL);
}

static fsm_state_t *build_implication(psl_fsm_t *fsm, fsm_state_t *state,
psl_node_t p)
static fsm_state_t *build_logical(psl_fsm_t *fsm, fsm_state_t *state,
psl_node_t p)
{
psl_node_t lhs = psl_operand(p, 0);
psl_node_t rhs = psl_operand(p, 1);

if (psl_subkind(p) == PSL_IMPL_IFF) {
// Only legal with Boolean HDL expression
fsm_state_t *left = add_state(fsm, p);
fsm_state_t *right = add_state(fsm, p);
fsm_state_t *accept = add_state(fsm, p);
add_edge(state, left, EDGE_EPSILON, lhs);
add_edge(state, right, EDGE_EPSILON, rhs);
add_edge(left, accept, EDGE_EPSILON, rhs);
add_edge(right, accept, EDGE_EPSILON, lhs);
add_edge(state, accept, EDGE_EPSILON, NULL);
return accept;
}
else {
fsm_state_t *left = add_state(fsm, p);
fsm_state_t *right = build_node(fsm, left, rhs);
add_edge(state, left, EDGE_EPSILON, lhs);
add_edge(state, right, EDGE_EPSILON, NULL);
return right;
switch (psl_subkind(p)) {
case PSL_LOGIC_IFF:
{
// Only legal with Boolean HDL expression
fsm_state_t *left = add_state(fsm, p);
fsm_state_t *right = add_state(fsm, p);
fsm_state_t *accept = add_state(fsm, p);
add_edge(state, left, EDGE_EPSILON, lhs);
add_edge(state, right, EDGE_EPSILON, rhs);
add_edge(left, accept, EDGE_EPSILON, rhs);
add_edge(right, accept, EDGE_EPSILON, lhs);
add_edge(state, accept, EDGE_EPSILON, NULL);
return accept;
}

case PSL_LOGIC_IF:
{
fsm_state_t *left = add_state(fsm, p);
fsm_state_t *right = build_node(fsm, left, rhs);
add_edge(state, left, EDGE_EPSILON, lhs);
add_edge(state, right, EDGE_EPSILON, NULL);
return right;
}

case PSL_LOGIC_OR:
{
fsm_state_t *accept = add_state(fsm, p), *final;

// At least one operand must be Boolean
if (psl_kind(lhs) == P_HDL_EXPR) {
add_edge(state, accept, EDGE_EPSILON, lhs);
final = build_node(fsm, state, rhs);
}
else {
add_edge(state, accept, EDGE_EPSILON, rhs);
final = build_node(fsm, state, lhs);
}

add_edge(final, accept, EDGE_EPSILON, NULL);
return accept;
}

default:
CANNOT_HANDLE(p);
}
}

Expand Down Expand Up @@ -269,8 +295,15 @@ static fsm_state_t *build_before(psl_fsm_t *fsm, fsm_state_t *state,

state->strong = !!(psl_flags(p) & PSL_F_STRONG);

add_edge(state, accept, EDGE_EPSILON, psl_operand(p, 0));
add_edge(state, fail, EDGE_EPSILON, psl_operand(p, 1));
if (psl_flags(p) & PSL_F_INCLUSIVE) {
add_edge(state, accept, EDGE_EPSILON, psl_operand(p, 0));
add_edge(state, fail, EDGE_EPSILON, psl_operand(p, 1));
}
else {
add_edge(state, fail, EDGE_EPSILON, psl_operand(p, 1));
add_edge(state, accept, EDGE_EPSILON, psl_operand(p, 0));
}

add_edge(state, state, EDGE_NEXT, NULL);

return accept;
Expand Down Expand Up @@ -318,8 +351,8 @@ static fsm_state_t *build_node(psl_fsm_t *fsm, fsm_state_t *state, psl_node_t p)
return build_next(fsm, state, p);
case P_SERE:
return build_sere(fsm, state, p);
case P_IMPLICATION:
return build_implication(fsm, state, p);
case P_LOGICAL:
return build_logical(fsm, state, p);
case P_UNTIL:
return build_until(fsm, state, p);
case P_EVENTUALLY:
Expand Down
12 changes: 6 additions & 6 deletions src/psl/psl-node.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,9 +71,6 @@ static const imask_t has_map[P_LAST_PSL_KIND] = {
// P_SERE
(I_SUBKIND | I_PARAMS | I_CLOCK | I_REPEAT | I_DECLS),

// P_IMPLICATION
(I_SUBKIND | I_PARAMS | I_CLOCK),

// P_REPEAT,
(I_SUBKIND | I_FOREIGN),

Expand Down Expand Up @@ -106,15 +103,18 @@ static const imask_t has_map[P_LAST_PSL_KIND] = {

// P_SUFFIX_IMPL
(I_SUBKIND | I_PARAMS | I_CLOCK),

// P_LOGICAL
(I_SUBKIND | I_PARAMS | I_CLOCK),
};

static const char *kind_text_map[P_LAST_PSL_KIND] = {
"P_ASSERT", "P_ASSUME", "P_RESTRICT", "P_FAIRNESS", "P_COVER", "P_ALWAYS",
"P_HDL_EXPR", "P_PROPERTY_DECL", "P_SEQUENCE_DECL", "P_CLOCK_DECL", "P_NEXT",
"P_NEVER", "P_EVENTUALLY", "P_NEXT_A", "P_NEXT_E", "P_NEXT_EVENT",
"P_SERE", "P_IMPLICATION", "P_REPEAT", "P_PROPERTY_INST", "P_SEQUENCE_INST",
"P_UNION", "P_BUILTIN_FUNC", "P_VALUE_SET", "P_PARAM", "P_UNTIL",
"P_ABORT", "P_BEFORE", "P_SUFFIX_IMPL",
"P_SERE", "P_REPEAT", "P_PROPERTY_INST", "P_SEQUENCE_INST", "P_UNION",
"P_BUILTIN_FUNC", "P_VALUE_SET", "P_PARAM", "P_UNTIL", "P_ABORT",
"P_BEFORE", "P_SUFFIX_IMPL", "P_LOGICAL",
};

static const change_allowed_t change_allowed[] = {
Expand Down
Loading

0 comments on commit ef8cfd0

Please sign in to comment.