Merge pull request #5141 from garytwong/unique-if

Accept (and ignore) SystemVerilog unique/priority if.

docs/source/yosys_internals/verilog.rst

@@ -375,3 +375,9 @@ from SystemVerilog:
   ports are inputs or outputs are supported.
 
 - Assignments within expressions are supported.
+
+- The ``unique``, ``unique0``, and ``priority`` SystemVerilog keywords are
+  accepted on ``if`` and ``case`` conditionals.  (Those keywords are currently
+  handled in the same way as their equivalent ``full_case`` and
+  ``parallel_case`` attributes on ``case`` statements, and checked
+  for syntactic validity but otherwise ignored on ``if`` statements.)

frontends/verilog/verilog_parser.y

@@ -426,7 +426,7 @@ static const AstNode *addAsgnBinopStmt(dict<IdString, AstNode*> *attr, AstNode *
 %type <boolean> opt_property always_comb_or_latch always_or_always_ff
 %type <boolean> opt_signedness_default_signed opt_signedness_default_unsigned
 %type <integer> integer_atom_type integer_vector_type
-%type <al> attr case_attr
+%type <al> attr if_attr case_attr
 %type <ast> struct_union
 %type <ast_node_type> asgn_binop inc_or_dec_op
 %type <ast> genvar_identifier
@@ -2871,7 +2871,7 @@ behavioral_stmt:
 		ast_stack.pop_back();
 		ast_stack.pop_back();
 	} |
-	attr TOK_IF '(' expr ')' {
+	if_attr TOK_IF '(' expr ')' {
 		AstNode *node = new AstNode(AST_CASE);
 		AstNode *block = new AstNode(AST_BLOCK);
 		AstNode *cond = new AstNode(AST_COND, AstNode::mkconst_int(1, false, 1), block);
@@ -2901,6 +2901,29 @@ behavioral_stmt:
 		ast_stack.pop_back();
 	};
 
+if_attr:
+	attr {
+		$$ = $1;
+	} |
+	attr TOK_UNIQUE0 {
+		AstNode *context = ast_stack.back();
+		if( context && context->type == AST_BLOCK && context->get_bool_attribute(ID::promoted_if) )
+			frontend_verilog_yyerror("unique0 keyword cannot be used for 'else if' branch.");
+		$$ = $1; // accept unique0 keyword, but ignore it for now
+	} |
+	attr TOK_PRIORITY {
+		AstNode *context = ast_stack.back();
+		if( context && context->type == AST_BLOCK && context->get_bool_attribute(ID::promoted_if) )
+			frontend_verilog_yyerror("priority keyword cannot be used for 'else if' branch.");
+		$$ = $1; // accept priority keyword, but ignore it for now
+	} |
+	attr TOK_UNIQUE {
+		AstNode *context = ast_stack.back();
+		if( context && context->type == AST_BLOCK && context->get_bool_attribute(ID::promoted_if) )
+			frontend_verilog_yyerror("unique keyword cannot be used for 'else if' branch.");
+		$$ = $1; // accept unique keyword, but ignore it for now
+	};
+
 case_attr:
 	attr {
 		$$ = $1;
@@ -2948,6 +2971,7 @@ behavioral_stmt_list:
 optional_else:
 	TOK_ELSE {
 		AstNode *block = new AstNode(AST_BLOCK);
+		block->attributes[ID::promoted_if] = AstNode::mkconst_int(1, false );
 		AstNode *cond = new AstNode(AST_COND, new AstNode(AST_DEFAULT), block);
 		SET_AST_NODE_LOC(cond, @1, @1);
 

kernel/constids.inc

@@ -153,6 +153,7 @@ X(parameter)
 X(PORTID)
 X(PRIORITY)
 X(PRIORITY_MASK)
+X(promoted_if)
 X(Q)
 X(R)
 X(ram_block)

tests/verilog/priority_if_enc.ys

@@ -0,0 +1,41 @@
+logger -expect log "SAT proof finished - no model found: SUCCESS" 1
+
+read_verilog -sv <<EOF
+// A somewhat contrived model of an encoder, relying on SystemVerilog's
+// strong "if" semantics to guarantee priority encoder behaviour.
+module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// Almost the same thing, but by using "priority if" we introduce
+// "don't care" states, essentially conveying permission to synthesise
+// a simple encoder instead.
+module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        priority if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// A simple test bench to detect mismatches between the two encoders.
+module compare_encoders( input [ 2:0 ] x, output ok );
+    wire [ 1:0 ] encout;
+    wire [ 1:0 ] dutout;
+    encoder e( x, encout );
+    dut d( x, dutout );
+    // The "priority if" above assumes $countones( x ) > 0.
+    assign ok = encout == dutout || !$countones( x );
+endmodule
+EOF
+
+synth -flatten -top compare_encoders
+sat -prove ok 1

tests/verilog/unique0_if_enc.ys

@@ -0,0 +1,41 @@
+logger -expect log "SAT proof finished - no model found: SUCCESS" 1
+
+read_verilog -sv <<EOF
+// A somewhat contrived model of an encoder, relying on SystemVerilog's
+// strong "if" semantics to guarantee priority encoder behaviour.
+module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// Almost the same thing, but by using "unique0 if" we introduce
+// "don't care" states, essentially conveying permission to synthesise
+// a simple encoder instead.
+module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        unique0 if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// A simple test bench to detect mismatches between the two encoders.
+module compare_encoders( input [ 2:0 ] x, output ok );
+    wire [ 1:0 ] encout;
+    wire [ 1:0 ] dutout;
+    encoder e( x, encout );
+    dut d( x, dutout );
+    // The "unique0 if" above assumes $onehot0( x ).
+    assign ok = encout == dutout || !$onehot0( x );
+endmodule
+EOF
+
+synth -flatten -top compare_encoders
+sat -prove ok 1

tests/verilog/unique_if.ys

@@ -0,0 +1,10 @@
+read_verilog -sv <<EOF
+module top( input[2:0] a );
+always_comb begin
+    // example from 1800-2012 12.4.2
+    unique if ((a==0) || (a==1)) $display("0 or 1");
+    else if (a == 2) $display("2");
+    else if (a == 4) $display("4");
+end
+endmodule
+EOF

tests/verilog/unique_if_else.ys

@@ -0,0 +1,11 @@
+logger -expect error "unique keyword cannot be used for 'else if' branch" 1
+read_verilog -sv <<EOF
+module top( input[2:0] a );
+always_comb begin
+    // invalid example from 1800-2012 12.4.2
+    unique if ((a==0) || (a==1)) $display("0 or 1");
+    else unique if (a == 2) $display("2");
+    else if (a == 4) $display("4");
+end
+endmodule
+EOF

tests/verilog/unique_if_else_begin.ys

@@ -0,0 +1,12 @@
+read_verilog -sv <<EOF
+module top( input[2:0] a );
+always_comb begin
+    // example from 1800-2012 12.4.2
+    unique if ((a==0) || (a==1)) $display("0 or 1");
+    else begin
+        unique if (a == 2) $display("2");
+        else if (a == 4) $display("4");
+    end
+end
+endmodule
+EOF

tests/verilog/unique_if_enc.ys

@@ -0,0 +1,41 @@
+logger -expect log "SAT proof finished - no model found: SUCCESS" 1
+
+read_verilog -sv <<EOF
+// A somewhat contrived model of an encoder, relying on SystemVerilog's
+// strong "if" semantics to guarantee priority encoder behaviour.
+module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// Almost the same thing, but by using "unique if" we introduce
+// "don't care" states, essentially conveying permission to synthesise
+// a simple encoder instead.
+module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        unique if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// A simple test bench to detect mismatches between the two encoders.
+module compare_encoders( input [ 2:0 ] x, output ok );
+    wire [ 1:0 ] encout;
+    wire [ 1:0 ] dutout;
+    encoder e( x, encout );
+    dut d( x, dutout );
+    // The "unique if" above assumes $onehot( x ).
+    assign ok = encout == dutout || !$onehot( x );
+endmodule
+EOF
+
+synth -flatten -top compare_encoders
+sat -prove ok 1