Merge branch 'YosysHQ:main' into main

This commit is contained in:
Akash Levy 2025-05-28 01:54:49 +02:00 committed by GitHub
commit 3fc74be3e2
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
15 changed files with 226 additions and 14 deletions

View File

@ -176,7 +176,7 @@ ifeq ($(OS), Haiku)
CXXFLAGS += -D_DEFAULT_SOURCE
endif
YOSYS_VER := 0.53+60
YOSYS_VER := 0.53+67
YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2)
YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'.' -f3)
@ -484,6 +484,7 @@ endif
ifeq ($(ENABLE_DEBUG),1)
CXXFLAGS := -Og -DDEBUG $(filter-out $(OPT_LEVEL),$(CXXFLAGS))
STRIP :=
endif
ifeq ($(ENABLE_ABC),1)
@ -1041,20 +1042,20 @@ install: $(TARGETS) $(EXTRA_TARGETS)
$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR)
$(INSTALL_SUDO) cp $(filter-out libyosys.so,$(TARGETS)) $(DESTDIR)$(BINDIR)
ifneq ($(filter $(PROGRAM_PREFIX)yosys,$(TARGETS)),)
$(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(BINDIR)/$(PROGRAM_PREFIX)yosys
if [ -n "$(STRIP)" ]; then $(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(BINDIR)/$(PROGRAM_PREFIX)yosys; fi
endif
ifneq ($(filter $(PROGRAM_PREFIX)yosys-abc,$(TARGETS)),)
$(INSTALL_SUDO) $(STRIP) $(DESTDIR)$(BINDIR)/$(PROGRAM_PREFIX)yosys-abc
if [ -n "$(STRIP)" ]; then $(INSTALL_SUDO) $(STRIP) $(DESTDIR)$(BINDIR)/$(PROGRAM_PREFIX)yosys-abc; fi
endif
ifneq ($(filter $(PROGRAM_PREFIX)yosys-filterlib,$(TARGETS)),)
$(INSTALL_SUDO) $(STRIP) $(DESTDIR)$(BINDIR)/$(PROGRAM_PREFIX)yosys-filterlib
if [ -n "$(STRIP)" ]; then $(INSTALL_SUDO) $(STRIP) $(DESTDIR)$(BINDIR)/$(PROGRAM_PREFIX)yosys-filterlib; fi
endif
$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(DATDIR)
$(INSTALL_SUDO) cp -r share/. $(DESTDIR)$(DATDIR)/.
ifeq ($(ENABLE_LIBYOSYS),1)
$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(LIBDIR)
$(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(LIBDIR)/
$(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(LIBDIR)/libyosys.so
if [ -n "$(STRIP)" ]; then $(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(LIBDIR)/libyosys.so; fi
ifeq ($(ENABLE_PYOSYS),1)
$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
$(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so

View File

@ -2429,8 +2429,6 @@ struct CxxrtlWorker {
inc_indent();
for (auto wire : module->wires()) {
const auto &debug_wire_type = debug_wire_types[wire];
if (!wire->name.isPublic())
continue;
count_public_wires++;
switch (debug_wire_type.type) {
case WireType::BUFFERED:
@ -2438,6 +2436,9 @@ struct CxxrtlWorker {
// Member wire
std::vector<std::string> flags;
if (!wire->name.isPublic())
flags.push_back("GENERATED");
if (wire->port_input && wire->port_output)
flags.push_back("INOUT");
else if (wire->port_output)

View File

@ -200,6 +200,10 @@ enum cxxrtl_flag {
// node, such as inputs and dangling wires.
CXXRTL_UNDRIVEN = 1 << 4,
// Generated correspond to netlist nodes that correspond to state with an internal name, that
// need to be saved, but wouldn't otherwise have a debug item generated.
CXXRTL_GENERATED = 1 << 5,
// More object flags may be added in the future, but the existing ones will never change.
};

View File

@ -1294,6 +1294,7 @@ struct debug_item : ::cxxrtl_object {
DRIVEN_SYNC = CXXRTL_DRIVEN_SYNC,
DRIVEN_COMB = CXXRTL_DRIVEN_COMB,
UNDRIVEN = CXXRTL_UNDRIVEN,
GENERATED = CXXRTL_GENERATED,
};
debug_item(const ::cxxrtl_object &object) : cxxrtl_object(object) {}

View File

@ -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.)

View File

@ -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);

View File

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

View File

@ -168,7 +168,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
vector<int> lut_costs, bool dff_mode, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode,
bool show_tempdir, std::string box_file, std::string lut_file,
std::vector<std::string> liberty_files, std::string wire_delay, std::string tempdir_name,
std::string constr_file, std::vector<std::string> dont_use_cells)
std::string constr_file, std::vector<std::string> dont_use_cells, std::vector<std::string> genlib_files)
{
std::string abc9_script;
@ -186,6 +186,10 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
}
if (!constr_file.empty())
abc9_script += stringf("read_constr -v \"%s\"; ", constr_file.c_str());
} else if (!genlib_files.empty()) {
for (std::string genlib_file : genlib_files) {
abc9_script += stringf("read_genlib \"%s\"; ", genlib_file.c_str());
}
}
log_assert(!box_file.empty());
@ -384,9 +388,14 @@ struct Abc9ExePass : public Pass {
log(" read the given Liberty file as a description of the target cell library.\n");
log(" this option can be used multiple times.\n");
log("\n");
log(" -genlib <file>\n");
log(" read the given genlib file as a description of the target cell library.\n");
log(" this option can be used multiple times.\n");
log("\n");
log(" -dont_use <cell_name>\n");
log(" avoid usage of the technology cell <cell_name> when mapping the design.\n");
log(" this option can be used multiple times.\n");
log(" this option can be used multiple times. only supported with Liberty\n");
log(" cell libraries.\n");
log("\n");
log(" -D <picoseconds>\n");
log(" set delay target. the string {D} in the default scripts above is\n");
@ -441,7 +450,7 @@ struct Abc9ExePass : public Pass {
std::string exe_file = yosys_abc_executable;
std::string script_file, clk_str, box_file, lut_file, constr_file;
std::vector<std::string> liberty_files, dont_use_cells;
std::vector<std::string> liberty_files, genlib_files, dont_use_cells;
std::string delay_target, lutin_shared = "-S 1", wire_delay;
std::string tempdir_name;
bool fast_mode = false, dff_mode = false;
@ -530,9 +539,15 @@ struct Abc9ExePass : public Pass {
continue;
}
if (arg == "-liberty" && argidx+1 < args.size()) {
rewrite_filename(args[argidx+1]);
liberty_files.push_back(args[++argidx]);
continue;
}
if (arg == "-genlib" && argidx+1 < args.size()) {
rewrite_filename(args[argidx+1]);
genlib_files.push_back(args[++argidx]);
continue;
}
if (arg == "-dont_use" && argidx+1 < args.size()) {
dont_use_cells.push_back(args[++argidx]);
continue;
@ -601,11 +616,13 @@ struct Abc9ExePass : public Pass {
if (tempdir_name.empty())
log_cmd_error("abc9_exe '-cwd' option is mandatory.\n");
if (!genlib_files.empty() && !dont_use_cells.empty())
log_cmd_error("abc9_exe '-genlib' is incompatible with '-dont_use'.\n");
abc9_module(design, script_file, exe_file, lut_costs, dff_mode,
delay_target, lutin_shared, fast_mode, show_tempdir,
box_file, lut_file, liberty_files, wire_delay, tempdir_name,
constr_file, dont_use_cells);
constr_file, dont_use_cells, genlib_files);
}
} Abc9ExePass;

View File

@ -68,6 +68,7 @@ struct AbcNewPass : public ScriptPass {
log(" -constr <file>\n");
log(" -dont_use <cell_name>\n");
log(" -liberty <file>\n");
log(" -genlib <file>\n");
log(" these options are passed on to the 'abc9_exe' command which invokes\n");
log(" the ABC tool on individual modules of the design. please see\n");
log(" 'help abc9_exe' for more details\n");
@ -90,7 +91,7 @@ struct AbcNewPass : public ScriptPass {
if (args[argidx] == "-exe" || args[argidx] == "-script" ||
args[argidx] == "-D" ||
args[argidx] == "-constr" || args[argidx] == "-dont_use" ||
args[argidx] == "-liberty") {
args[argidx] == "-liberty" || args[argidx] == "-genlib") {
abc_exe_options += " " + args[argidx] + " " + args[argidx + 1];
argidx++;
} else if (args[argidx] == "-run" && argidx + 1 < args.size()) {

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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