From 127e639d5391f8873ae3c7622a0764f7bbdc3968 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 25 Oct 2024 09:18:44 -0700 Subject: [PATCH] Verilog: grammar for combinational UDPs This adds the 1800-2017 grammar for user-defined combinational primitives. --- regression/verilog/UDPs/multiplexer1.desc | 7 ++ regression/verilog/UDPs/multiplexer1.sv | 25 +++++ src/verilog/parser.y | 127 ++++++++++++++++++---- 3 files changed, 140 insertions(+), 19 deletions(-) create mode 100644 regression/verilog/UDPs/multiplexer1.desc create mode 100644 regression/verilog/UDPs/multiplexer1.sv diff --git a/regression/verilog/UDPs/multiplexer1.desc b/regression/verilog/UDPs/multiplexer1.desc new file mode 100644 index 00000000..3efdf2ed --- /dev/null +++ b/regression/verilog/UDPs/multiplexer1.desc @@ -0,0 +1,7 @@ +CORE +multiplexer1.sv +--bound 0 --module main +^no properties$ +^EXIT=10$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/UDPs/multiplexer1.sv b/regression/verilog/UDPs/multiplexer1.sv new file mode 100644 index 00000000..174390db --- /dev/null +++ b/regression/verilog/UDPs/multiplexer1.sv @@ -0,0 +1,25 @@ +// 1800-2017 29.4 +primitive multiplexer (mux, control, dataA, dataB); + output mux; + input control, dataA, dataB; + table + // control dataA dataB mux + 0 1 0 : 1 ; + 0 1 1 : 1 ; + 0 1 x : 1 ; + 0 0 0 : 0 ; + 0 0 1 : 0 ; + 0 0 x : 0 ; + 1 0 1 : 1 ; + 1 1 1 : 1 ; + 1 x 1 : 1 ; + 1 0 0 : 0 ; + 1 1 0 : 0 ; + 1 x 0 : 0 ; + x 0 0 : 0 ; + x 1 1 : 1 ; + endtable +endprimitive + +module main; +endmodule diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 954744bb..26124c15 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -771,6 +771,12 @@ parameter_port_list_opt: { init($$); } ; +list_of_ports_opt: + /* Optional */ + { make_nil($$); } + | list_of_ports + ; + list_of_ports: '(' port_brace ')' { $$ = $2; } ; @@ -2770,14 +2776,34 @@ constant_expression: expression; // System Verilog standard 1800-2017 // A.5.1 UDP declaration -udp_declaration: attribute_instance_brace TOK_PRIMITIVE udp_identifier - '(' udp_port_list ')' ';' udp_port_declaration_brace - udp_body TOK_ENDPRIMITIVE - | attribute_instance_brace TOK_PRIMITIVE udp_identifier - '(' udp_declaration_port_list ')' ';' - udp_body TOK_ENDPRIMITIVE +udp_nonansi_declaration: + attribute_instance_brace + TOK_PRIMITIVE udp_identifier '(' udp_port_list ')' ';' ; +udp_ansi_declaration: + attribute_instance_brace + TOK_PRIMITIVE udp_identifier '(' udp_declaration_port_list ')' ';' + ; + +udp_declaration: + udp_nonansi_declaration + udp_port_declaration + udp_port_declaration_brace + udp_body + TOK_ENDPRIMITIVE + | udp_ansi_declaration + udp_body + TOK_ENDPRIMITIVE + | TOK_EXTERN udp_nonansi_declaration + | TOK_EXTERN udp_ansi_declaration + | attribute_instance_brace + TOK_PRIMITIVE udp_identifier '(' ')' ';' + udp_port_declaration_brace + udp_body + TOK_ENDPRIMITIVE + ; + // System Verilog standard 1800-2017 // A.5.2 UDP ports @@ -2823,31 +2849,94 @@ port_identifier_brace: // System Verilog standard 1800-2017 // A.5.3 UDP body -udp_body: udp_initial_statement_opt TOK_TABLE table_entry_brace TOK_ENDTABLE +udp_body: combinational_body ; + +combinational_body: + TOK_TABLE + combinational_entry_brace + TOK_ENDTABLE + ; + +combinational_entry_brace: + combinational_entry + | combinational_entry_brace combinational_entry + ; + +combinational_entry: + level_input_list TOK_COLON output_symbol ';' + ; + +sequential_body: + udp_initial_statement_opt + TOK_TABLE sequential_entry_brace TOK_ENDTABLE ; udp_initial_statement_opt: + /* Optional */ + | udp_initial_statement ; -table_entry_brace: - table_entry - | table_entry_brace table_entry +udp_initial_statement: + TOK_INITIAL output_port_identifier '=' init_val ';' ; -table_entry: input_list TOK_COLON output_or_level_symbol ';' - | input_list TOK_COLON output_or_level_symbol TOK_COLON next_state ';' +output_port_identifier: new_identifier ; -input_list:; +init_val: + // Really 1'b0 | 1'b1 | 1'bx | 1'bX | 1'B0 | 1'B1 | 1'Bx | 1'BX | 1 | 0 + TOK_NUMBER + | new_identifier + ; -output_or_level_symbol:; +sequential_entry_brace: + sequential_entry + | sequential_entry_brace sequential_entry + ; -next_state:; +sequential_entry: + seq_input_list TOK_COLON current_state TOK_COLON next_state + ; -list_of_ports_opt: - /* Optional */ - { make_nil($$); } - | list_of_ports +seq_input_list: level_input_list | edge_input_list + ; + +edge_indicator: + '(' level_symbol level_symbol ')' | edge_symbol + ; + +current_state: level_symbol ; + +next_state: output_symbol | '-' ; + +level_input_list: + level_symbol + | level_input_list level_symbol + ; + +edge_input_list: level_symbol_brace edge_indicator level_symbol_brace ; + +output_symbol: + // Really 0 | 1 | x | X + TOK_NUMBER + | new_identifier + ; + +level_symbol_brace: + level_symbol + | level_symbol_brace level_symbol + ; + +level_symbol: + // Really 0 | 1 | x | X | ? | b | B + TOK_NUMBER + | new_identifier + ; + +edge_symbol: + // Really r | R | f | F | p | P | n | N | * + TOK_NUMBER + | new_identifier ; // System Verilog standard 1800-2017