From 13f411b8c7dc3580dc3a2fbf1cc075583ec9cac6 Mon Sep 17 00:00:00 2001 From: Blebowski <34539154+Blebowski@users.noreply.github.com> Date: Wed, 15 Mar 2023 18:13:50 +0100 Subject: [PATCH] Parse "assume_directive", "cover_directive" and optional "report". (#649) --- src/lexer.l | 14 ++++ src/parse.c | 153 +++++++++++++++++++++++++++++++++++++++++++- src/psl/psl-dump.c | 47 ++++++++++++++ src/psl/psl-node.c | 38 +++++++++-- src/psl/psl-node.h | 13 ++++ src/psl/psl-sem.c | 36 +++++++++++ src/scan.h | 7 ++ test/psl/parse3.vhd | 15 +++++ test/test_psl.c | 12 ++++ 9 files changed, 330 insertions(+), 5 deletions(-) diff --git a/src/lexer.l b/src/lexer.l index 269f7832..a098840e 100644 --- a/src/lexer.l +++ b/src/lexer.l @@ -226,6 +226,13 @@ EVENTUALLY ?i:eventually NEXT_A ?i:next_a NEXT_E ?i:next_e NEXT_EVENT ?i:next_event +ASSUME ?i:assume +ASSUME_G ?i:assume_guarantee +RESTRICT ?i:restrict +RESTRICT_G ?i:restrict_guarantee +STRONG ?i:strong +FAIRNESS ?i:fairness +COVER ?i:cover %% @@ -423,6 +430,13 @@ NEXT_EVENT ?i:next_event ">=" { TOKEN(tGE); } {ASSERT} { TOKEN(tASSERT); } +{ASSUME} { TOKEN(tASSUME); } +{ASSUME_G} { TOKEN(tASSUMEG); } +{RESTRICT} { TOKEN(tRESTRICT); } +{RESTRICT_G} { TOKEN(tRESTRICTG); } +{STRONG} { TOKEN(tSTRONG); } +{FAIRNESS} { TOKEN(tFAIRNESS); } +{COVER} { TOKEN(tCOVER); } {ALWAYS} { TOKEN(tALWAYS); } {DEFAULT} { TOKEN(tDEFAULT); } {CLOCK} { TOKEN(tCLOCK); } diff --git a/src/parse.c b/src/parse.c index 1ba1ad52..b55343db 100644 --- a/src/parse.c +++ b/src/parse.c @@ -10231,6 +10231,15 @@ static psl_node_t p_psl_fl_property(void) } } +static void p_psl_report(psl_node_t p) +{ + consume(tREPORT); + + tree_t m = p_expression(); + psl_set_message(p, m); + solve_types(nametab, m, std_type(NULL, STD_STRING)); +} + static psl_node_t p_psl_property(void) { // Replicator Property | FL_Property | OBE_Property @@ -10255,6 +10264,137 @@ static psl_node_t p_psl_assert_directive(void) psl_node_t a = psl_new(P_ASSERT); psl_set_value(a, p); + if (peek() == tREPORT) + p_psl_report(a); + + consume(tSEMI); + + psl_set_loc(a, CURRENT_LOC); + return a; +} + +static psl_node_t p_psl_assume_directive(void) +{ + // assume Property ; + // assume_guarantee Property [ report String ] ; + + BEGIN("assume directive"); + + token_t tok = one_of(tASSUME, tASSUMEG); + + psl_node_t a = psl_new(P_ASSUME); + if (tok == tASSUME) + psl_set_subkind(a, PSL_NO_GUARANTEE); + else + psl_set_subkind(a, PSL_GUARANTEE); + + psl_node_t p = p_psl_property(); + if (!psl_has_clock(p)) + psl_set_clock(p, find_default_clock(nametab)); + psl_set_value(a, p); + + if (peek() == tREPORT && tok == tASSUMEG) + p_psl_report(a); + + consume(tSEMI); + + psl_set_loc(a, CURRENT_LOC); + return a; +} + +static psl_node_t p_psl_restrict_directive(void) +{ + // restrict Sequence ; + // restrict_guarantee Sequence [ report String ] ; + + BEGIN("restrict directive"); + + token_t tok = peek(); + assert(tok == tRESTRICT || tok == tRESTRICTG); + consume(tok); + + psl_node_t a = psl_new(P_RESTRICT); + if (tok == tRESTRICT) + psl_set_subkind(a, PSL_NO_GUARANTEE); + else + psl_set_subkind(a, PSL_GUARANTEE); + + psl_node_t p = p_psl_sequence(); + if (!psl_has_clock(p)) + psl_set_clock(p, find_default_clock(nametab)); + psl_set_value(a, p); + + if (peek() == tREPORT && tok == tRESTRICTG) + p_psl_report(a); + + consume(tSEMI); + + psl_set_loc(a, CURRENT_LOC); + return a; +} + +static psl_node_t p_psl_fairness(void) +{ + // fairness Boolean ; + // strong fairness Boolean , Boolean ; + + BEGIN("fairness statement"); + + psl_strength_t strength = PSL_WEAK; + if (peek() == tSTRONG) { + consume(tSTRONG); + strength = PSL_STRONG; + } + + consume(tFAIRNESS); + + psl_node_t a = psl_new(P_FAIRNESS); + psl_set_subkind(a, strength); + + tree_t e1 = p_expression(); + solve_psl_condition(nametab, e1); + + psl_node_t p1 = psl_new(P_HDL_EXPR); + psl_set_tree(p1, e1); + + psl_add_operand(a, p1); + + if (strength == PSL_STRONG) { + consume(tCOMMA); + + tree_t e2 = p_expression(); + solve_psl_condition(nametab, e2); + + psl_node_t p2 = psl_new(P_HDL_EXPR); + psl_set_tree(p2, e2); + + psl_add_operand(a, p2); + } + + consume(tSEMI); + + psl_set_loc(a, CURRENT_LOC); + return a; +} + +static psl_node_t p_psl_cover_directive(void) +{ + // cover Sequence [ report String ] ; + + BEGIN("cover directive"); + + consume(tCOVER); + + psl_node_t p = p_psl_sequence(); + if (!psl_has_clock(p)) + psl_set_clock(p, find_default_clock(nametab)); + + psl_node_t a = psl_new(P_COVER); + psl_set_value(a, p); + + if (peek() == tREPORT) + p_psl_report(a); + consume(tSEMI); psl_set_loc(a, CURRENT_LOC); @@ -10271,8 +10411,19 @@ static psl_node_t p_psl_verification_directive(void) switch (peek()) { case tASSERT: return p_psl_assert_directive(); + case tASSUME: + case tASSUMEG: + return p_psl_assume_directive(); + case tRESTRICT: + case tRESTRICTG: + return p_psl_restrict_directive(); + case tFAIRNESS: + case tSTRONG: + return p_psl_fairness(); + case tCOVER: + return p_psl_cover_directive(); default: - one_of(tASSERT); + one_of(tASSERT, tASSUME, tCOVER); return NULL; } } diff --git a/src/psl/psl-dump.c b/src/psl/psl-dump.c index edd36266..0adf73bb 100644 --- a/src/psl/psl-dump.c +++ b/src/psl/psl-dump.c @@ -30,6 +30,41 @@ static void psl_dump_assert(psl_node_t p) psl_dump(psl_value(p)); } +static void psl_dump_assume(psl_node_t p) +{ + if (psl_subkind(p) == PSL_GUARANTEE) + print_syntax("#assume guarantee"); + else + print_syntax("#assume"); + psl_dump(psl_value(p)); +} + +static void psl_dump_restrict(psl_node_t p) +{ + if (psl_subkind(p) == PSL_GUARANTEE) + print_syntax("#restrict guarantee"); + else + print_syntax("#restrict"); + psl_dump(psl_value(p)); +} + +static void psl_dump_fairness(psl_node_t p) +{ + if (psl_subkind(p) == PSL_STRONG) + print_syntax("#strong fairness"); + else + print_syntax("#fairness"); + + for (int i = 0; i < psl_operands(p); i++) + psl_dump(psl_operand(p, i)); +} + +static void psl_dump_cover(psl_node_t p) +{ + print_syntax("#cover"); + psl_dump(psl_value(p)); +} + static void psl_dump_always(psl_node_t p) { print_syntax("#always "); @@ -94,6 +129,18 @@ void psl_dump(psl_node_t p) case P_ASSERT: psl_dump_assert(p); break; + case P_ASSUME: + psl_dump_assume(p); + break; + case P_RESTRICT: + psl_dump_restrict(p); + break; + case P_FAIRNESS: + psl_dump_fairness(p); + break; + case P_COVER: + psl_dump_cover(p); + break; case P_ALWAYS: psl_dump_always(p); break; diff --git a/src/psl/psl-node.c b/src/psl/psl-node.c index fc462e04..e3aee1b6 100644 --- a/src/psl/psl-node.c +++ b/src/psl/psl-node.c @@ -21,7 +21,19 @@ static const imask_t has_map[P_LAST_PSL_KIND] = { // P_ASSERT - (I_VALUE), + (I_VALUE | I_MESSAGE), + + // P_ASSUME + (I_SUBKIND | I_VALUE | I_MESSAGE), + + // P_RESTRICT + (I_SUBKIND | I_VALUE | I_MESSAGE), + + // P_FAIRNESS + (I_SUBKIND | I_PARAMS | I_MESSAGE), + + // P_COVER + (I_VALUE | I_MESSAGE), // P_ALWAYS (I_VALUE | I_CLOCK), @@ -58,9 +70,9 @@ static const imask_t has_map[P_LAST_PSL_KIND] = { }; static const char *kind_text_map[P_LAST_PSL_KIND] = { - "P_ASSERT", "P_ALWAYS", "P_HDL_EXPR", "P_CLOCK_DECL", "P_NEXT", - "P_NEVER", "P_EVENTUALLY", "P_NEXT_A", "P_NEXT_E", "P_NEXT_EVENT", - "P_SERE", "P_IMPLICATION", + "P_ASSERT", "P_ASSUME", "P_RESTRICT", "P_FAIRNESS", "P_COVER", "P_ALWAYS", + "P_HDL_EXPR", "P_CLOCK_DECL", "P_NEXT", "P_NEVER", "P_EVENTUALLY", + "P_NEXT_A", "P_NEXT_E", "P_NEXT_EVENT", "P_SERE", "P_IMPLICATION", }; static const change_allowed_t change_allowed[] = { @@ -209,6 +221,24 @@ void psl_set_clock(psl_node_t p, psl_node_t clk) object_write_barrier(&(p->object), &(clk->object)); } +tree_t psl_message(psl_node_t p) +{ + item_t *item = lookup_item(&psl_object, p, I_MESSAGE); + assert(item->object != NULL); + return container_of(item->object, struct _tree, object); +} + +bool psl_has_message(psl_node_t p) +{ + return lookup_item(&psl_object, p, I_MESSAGE)->object != NULL; +} + +void psl_set_message(psl_node_t p, tree_t m) +{ + lookup_item(&psl_object, p, I_MESSAGE)->object = &(m->object); + object_write_barrier(&(p->object), &(m->object)); +} + object_t *psl_to_object(psl_node_t p) { return &(p->object); diff --git a/src/psl/psl-node.h b/src/psl/psl-node.h index 7a808178..9b47688d 100644 --- a/src/psl/psl-node.h +++ b/src/psl/psl-node.h @@ -22,6 +22,10 @@ typedef enum { P_ASSERT, + P_ASSUME, + P_RESTRICT, + P_FAIRNESS, + P_COVER, P_ALWAYS, P_HDL_EXPR, P_CLOCK_DECL, @@ -55,6 +59,11 @@ typedef enum { PSL_STRONG, } psl_strength_t; +typedef enum { + PSL_GUARANTEE, + PSL_NO_GUARANTEE, +} psl_guarantee_t; + psl_node_t psl_new(psl_kind_t kind); psl_kind_t psl_kind(psl_node_t p); const char *psl_kind_str(psl_kind_t kind); @@ -82,6 +91,10 @@ psl_node_t psl_clock(psl_node_t p); bool psl_has_clock(psl_node_t p); void psl_set_clock(psl_node_t p, psl_node_t clk); +tree_t psl_message(psl_node_t p); +bool psl_has_message(psl_node_t p); +void psl_set_message(psl_node_t, tree_t m); + object_t *psl_to_object(psl_node_t p); psl_node_t psl_from_object(object_t *obj); diff --git a/src/psl/psl-sem.c b/src/psl/psl-sem.c index 1e5fad77..68343dff 100644 --- a/src/psl/psl-sem.c +++ b/src/psl/psl-sem.c @@ -29,6 +29,26 @@ static void psl_check_assert(psl_node_t p) } +static void psl_check_assume(psl_node_t p) +{ + +} + +static void psl_check_restrict(psl_node_t p) +{ + +} + +static void psl_check_fairness(psl_node_t p) +{ + +} + +static void psl_check_cover(psl_node_t p) +{ + +} + static void psl_check_always(psl_node_t p) { @@ -50,6 +70,22 @@ void psl_check(psl_node_t p) psl_check_assert(p); break; + case P_ASSUME: + psl_check_assume(p); + break; + + case P_RESTRICT: + psl_check_restrict(p); + break; + + case P_FAIRNESS: + psl_check_fairness(p); + break; + + case P_COVER: + psl_check_cover(p); + break; + case P_CLOCK_DECL: psl_check_clock_decl(p); break; diff --git a/src/scan.h b/src/scan.h index 641313e7..23b38a2a 100644 --- a/src/scan.h +++ b/src/scan.h @@ -246,5 +246,12 @@ void reset_verilog_parser(void); #define tINITIAL 357 #define tWIRE 358 #define tUNSIGNED 359 +#define tASSUME 360 +#define tASSUMEG 361 +#define tRESTRICT 362 +#define tRESTRICTG 363 +#define tSTRONG 364 +#define tFAIRNESS 365 +#define tCOVER 366 #endif // _SCAN_H diff --git a/test/psl/parse3.vhd b/test/psl/parse3.vhd index f98dbb69..a867134c 100644 --- a/test/psl/parse3.vhd +++ b/test/psl/parse3.vhd @@ -14,4 +14,19 @@ begin -- psl assert {a}; -- psl assert {a;b and c}; + -- psl cover {a ; b;c }; + -- psl named_cover : cover {c} report "'c' is covered"; + + -- psl assume b; + -- psl named_assume : assume (a -> b); + -- psl assume_guarantee ( b -> c) report "assume_guarantee met"; + + -- psl restrict {c ;b ; c; b}; + -- psl named_restrict : restrict {c}; + -- psl restrict_guarantee {b; b} report "restrict_guarantee met"; + + -- psl fairness (b = '1'); + -- psl named_fairness : fairness (a = '1'); + -- psl strong fairness (a = '1'), (b = '1'); + end architecture; diff --git a/test/test_psl.c b/test/test_psl.c index 8ce990a5..ac54f1b4 100644 --- a/test/test_psl.c +++ b/test/test_psl.c @@ -121,6 +121,18 @@ START_TEST(test_parse3) fail_unless(psl_kind(p0) == P_ASSERT); fail_unless(psl_has_clock(psl_value(p0))); + psl_node_t p1 = tree_psl(tree_stmt(a, 7)); + fail_unless(psl_kind(p1) == P_COVER); + + psl_node_t p2 = tree_psl(tree_stmt(a, 9)); + fail_unless(psl_kind(p2) == P_ASSUME); + + psl_node_t p3 = tree_psl(tree_stmt(a, 12)); + fail_unless(psl_kind(p3) == P_RESTRICT); + + psl_node_t p4 = tree_psl(tree_stmt(a, 15)); + fail_unless(psl_kind(p4) == P_FAIRNESS); + fail_if_errors(); } END_TEST -- 2.39.2