From 0a6d9f4dc993dc8d7d68204681ed83e56fa9c77a Mon Sep 17 00:00:00 2001 From: Sean Luchen Date: Mon, 31 Mar 2025 10:44:23 -0700 Subject: [PATCH 01/11] Factor report_unexpected_token out into its own function. --- passes/techmap/libparse.cc | 69 ++++++++++++++++---------------------- passes/techmap/libparse.h | 1 + 2 files changed, 30 insertions(+), 40 deletions(-) diff --git a/passes/techmap/libparse.cc b/passes/techmap/libparse.cc index 06dd6288e..afc49b454 100644 --- a/passes/techmap/libparse.cc +++ b/passes/techmap/libparse.cc @@ -332,6 +332,32 @@ int LibertyParser::lexer(std::string &str) return c; } +void LibertyParser::report_unexpected_token(int tok) +{ + std::string eReport; + switch(tok) + { + case 'n': + error("Unexpected newline."); + break; + case '[': + case ']': + case '}': + case '{': + case '\"': + case ':': + eReport = "Unexpected '"; + eReport += static_cast(tok); + eReport += "'."; + error(eReport); + break; + default: + eReport = "Unexpected token: "; + eReport += static_cast(tok); + error(eReport); + } +} + LibertyAst *LibertyParser::parse() { std::string str; @@ -350,26 +376,7 @@ LibertyAst *LibertyParser::parse() return NULL; if (tok != 'v') { - std::string eReport; - switch(tok) - { - case 'n': - error("Unexpected newline."); - break; - case '[': - case ']': - case '}': - case '{': - case '\"': - case ':': - eReport = "Unexpected '"; - eReport += static_cast(tok); - eReport += "'."; - error(eReport); - break; - default: - error(); - } + report_unexpected_token(tok); } LibertyAst *ast = new LibertyAst; @@ -460,25 +467,7 @@ LibertyAst *LibertyParser::parse() continue; } if (tok != 'v') { - std::string eReport; - switch(tok) - { - case 'n': - continue; - case '[': - case ']': - case '}': - case '{': - case '\"': - case ':': - eReport = "Unexpected '"; - eReport += static_cast(tok); - eReport += "'."; - error(eReport); - break; - default: - error(); - } + report_unexpected_token(tok); } ast->args.push_back(arg); } @@ -495,7 +484,7 @@ LibertyAst *LibertyParser::parse() break; } - error(); + report_unexpected_token(tok); } return ast; diff --git a/passes/techmap/libparse.h b/passes/techmap/libparse.h index 16808fc58..ea81abe2f 100644 --- a/passes/techmap/libparse.h +++ b/passes/techmap/libparse.h @@ -105,6 +105,7 @@ namespace Yosys */ int lexer(std::string &str); + void report_unexpected_token(int tok); LibertyAst *parse(); void error() const; void error(const std::string &str) const; From ac1033ecd554b5685f89167ce240ab6fee60ca4c Mon Sep 17 00:00:00 2001 From: Sean Luchen Date: Mon, 31 Mar 2025 10:46:18 -0700 Subject: [PATCH 02/11] Factor parse_vector_range out into its own function. This also fixes the parsing a bit. It was consuming 1 fewer token than required. --- passes/techmap/libparse.cc | 80 ++++++++++++++++++++------------------ passes/techmap/libparse.h | 1 + 2 files changed, 44 insertions(+), 37 deletions(-) diff --git a/passes/techmap/libparse.cc b/passes/techmap/libparse.cc index afc49b454..09afcf9f3 100644 --- a/passes/techmap/libparse.cc +++ b/passes/techmap/libparse.cc @@ -358,6 +358,48 @@ void LibertyParser::report_unexpected_token(int tok) } } +// FIXME: the AST needs to be extended to store +// these vector ranges. +int LibertyParser::parse_vector_range(int tok) +{ + // parse vector range [A] or [A:B] + std::string arg; + tok = lexer(arg); + if (tok != 'v') + { + // expected a vector array index + error("Expected a number."); + } + else + { + // fixme: check for number A + } + tok = lexer(arg); + // optionally check for : in case of [A:B] + // if it isn't we just expect ']' + // as we have [A] + if (tok == ':') + { + tok = lexer(arg); + if (tok != 'v') + { + // expected a vector array index + error("Expected a number."); + } + else + { + // fixme: check for number B + tok = lexer(arg); + } + } + // expect a closing bracket of array range + if (tok != ']') + { + error("Expected ']' on array range."); + } + return lexer(arg); +} + LibertyAst *LibertyParser::parse() { std::string str; @@ -425,45 +467,9 @@ LibertyAst *LibertyParser::parse() if (tok == ')') break; - // FIXME: the AST needs to be extended to store - // these vector ranges. if (tok == '[') { - // parse vector range [A] or [A:B] - std::string arg; - tok = lexer(arg); - if (tok != 'v') - { - // expected a vector array index - error("Expected a number."); - } - else - { - // fixme: check for number A - } - tok = lexer(arg); - // optionally check for : in case of [A:B] - // if it isn't we just expect ']' - // as we have [A] - if (tok == ':') - { - tok = lexer(arg); - if (tok != 'v') - { - // expected a vector array index - error("Expected a number."); - } - else - { - // fixme: check for number B - tok = lexer(arg); - } - } - // expect a closing bracket of array range - if (tok != ']') - { - error("Expected ']' on array range."); - } + tok = parse_vector_range(tok); continue; } if (tok != 'v') { diff --git a/passes/techmap/libparse.h b/passes/techmap/libparse.h index ea81abe2f..686a2b49f 100644 --- a/passes/techmap/libparse.h +++ b/passes/techmap/libparse.h @@ -106,6 +106,7 @@ namespace Yosys int lexer(std::string &str); void report_unexpected_token(int tok); + int parse_vector_range(int tok); LibertyAst *parse(); void error() const; void error(const std::string &str) const; From 23f59e0196fd6275f1f6267f59ed7f358704c9f5 Mon Sep 17 00:00:00 2001 From: Sean Luchen Date: Mon, 31 Mar 2025 10:47:39 -0700 Subject: [PATCH 03/11] Support array ranges for identifiers in the Liberty parser. This change only handles the case `id : id[range] ;`. --- passes/techmap/libparse.cc | 4 +++- passes/techmap/libparse.h | 4 ++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/passes/techmap/libparse.cc b/passes/techmap/libparse.cc index 09afcf9f3..d85e9d915 100644 --- a/passes/techmap/libparse.cc +++ b/passes/techmap/libparse.cc @@ -436,7 +436,9 @@ LibertyAst *LibertyParser::parse() if (tok == ':' && ast->value.empty()) { tok = lexer(ast->value); if (tok == 'v') { - tok = lexer(str); + tok = lexer(str); + if (tok == '[') + tok = parse_vector_range(tok); } while (tok == '+' || tok == '-' || tok == '*' || tok == '/' || tok == '!') { ast->value += tok; diff --git a/passes/techmap/libparse.h b/passes/techmap/libparse.h index 686a2b49f..61ae4d334 100644 --- a/passes/techmap/libparse.h +++ b/passes/techmap/libparse.h @@ -105,8 +105,8 @@ namespace Yosys */ int lexer(std::string &str); - void report_unexpected_token(int tok); - int parse_vector_range(int tok); + void report_unexpected_token(int tok); + int parse_vector_range(int tok); LibertyAst *parse(); void error() const; void error(const std::string &str) const; From 4610889d27627fdd6dc01518e07fd617e317eeac Mon Sep 17 00:00:00 2001 From: Sean Luchen Date: Tue, 1 Apr 2025 13:01:00 -0700 Subject: [PATCH 04/11] Fix two parsing bugs that were causing private regression tests to fail. These were introduced by 0a6d9f4. 1) While in a paren "(", don't error on newline. 2) Don't parse an extra token when parsing vector ranges. Let the caller parse the next token as necessary. --- passes/techmap/libparse.cc | 13 ++++++++----- passes/techmap/libparse.h | 2 +- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/passes/techmap/libparse.cc b/passes/techmap/libparse.cc index d85e9d915..e5ed094b3 100644 --- a/passes/techmap/libparse.cc +++ b/passes/techmap/libparse.cc @@ -360,7 +360,7 @@ void LibertyParser::report_unexpected_token(int tok) // FIXME: the AST needs to be extended to store // these vector ranges. -int LibertyParser::parse_vector_range(int tok) +void LibertyParser::parse_vector_range(int tok) { // parse vector range [A] or [A:B] std::string arg; @@ -397,7 +397,6 @@ int LibertyParser::parse_vector_range(int tok) { error("Expected ']' on array range."); } - return lexer(arg); } LibertyAst *LibertyParser::parse() @@ -437,8 +436,10 @@ LibertyAst *LibertyParser::parse() tok = lexer(ast->value); if (tok == 'v') { tok = lexer(str); - if (tok == '[') - tok = parse_vector_range(tok); + if (tok == '[') { + parse_vector_range(tok); + tok = lexer(str); + } } while (tok == '+' || tok == '-' || tok == '*' || tok == '/' || tok == '!') { ast->value += tok; @@ -471,9 +472,11 @@ LibertyAst *LibertyParser::parse() if (tok == '[') { - tok = parse_vector_range(tok); + parse_vector_range(tok); continue; } + if (tok == 'n') + continue; if (tok != 'v') { report_unexpected_token(tok); } diff --git a/passes/techmap/libparse.h b/passes/techmap/libparse.h index 61ae4d334..2f0678513 100644 --- a/passes/techmap/libparse.h +++ b/passes/techmap/libparse.h @@ -106,7 +106,7 @@ namespace Yosys int lexer(std::string &str); void report_unexpected_token(int tok); - int parse_vector_range(int tok); + void parse_vector_range(int tok); LibertyAst *parse(); void error() const; void error(const std::string &str) const; From bdcbbf2db63297b7f137b0a3371c666f1000a42f Mon Sep 17 00:00:00 2001 From: Sean Luchen Date: Thu, 3 Apr 2025 09:56:24 -0700 Subject: [PATCH 05/11] Fix existing tests/liberty tests, and add them to Makefile. --- Makefile | 1 + tests/liberty/XNOR2X1.lib.filtered.ok | 2 +- tests/liberty/XNOR2X1.lib.verilogsim.ok | 2 +- tests/liberty/normal.lib.filtered.ok | 50 ++++++++-------- tests/liberty/normal.lib.verilogsim.ok | 60 +++++++++---------- tests/liberty/run-test.sh | 5 +- tests/liberty/semicolextra.lib.filtered.ok | 4 +- tests/liberty/semicolextra.lib.verilogsim.ok | 2 +- tests/liberty/semicolmissing.lib.filtered.ok | 4 +- .../liberty/semicolmissing.lib.verilogsim.ok | 4 +- 10 files changed, 68 insertions(+), 66 deletions(-) diff --git a/Makefile b/Makefile index 74128b41d..340186470 100644 --- a/Makefile +++ b/Makefile @@ -889,6 +889,7 @@ SH_TEST_DIRS += tests/rpc SH_TEST_DIRS += tests/memfile SH_TEST_DIRS += tests/fmt SH_TEST_DIRS += tests/cxxrtl +SH_TEST_DIRS += tests/liberty ifeq ($(ENABLE_FUNCTIONAL_TESTS),1) SH_TEST_DIRS += tests/functional endif diff --git a/tests/liberty/XNOR2X1.lib.filtered.ok b/tests/liberty/XNOR2X1.lib.filtered.ok index 14e9b625d..5ca81b2d7 100644 --- a/tests/liberty/XNOR2X1.lib.filtered.ok +++ b/tests/liberty/XNOR2X1.lib.filtered.ok @@ -9,7 +9,7 @@ library(ls05_stdcells) { } pin(Y) { direction : output ; - function : !(B&!A|!B&A) ; + function : "!(B&!A|!B&A)" ; } } } diff --git a/tests/liberty/XNOR2X1.lib.verilogsim.ok b/tests/liberty/XNOR2X1.lib.verilogsim.ok index 62c9f7ffa..89e55e8b8 100644 --- a/tests/liberty/XNOR2X1.lib.verilogsim.ok +++ b/tests/liberty/XNOR2X1.lib.verilogsim.ok @@ -2,5 +2,5 @@ module XNOR2X1 (B, A, Y); input B; input A; output Y; - assign Y = !(B&!A|!B&A); // !(B&!A|!B&A) + assign Y = !(B&!A|!B&A); // "!(B&!A|!B&A)" endmodule diff --git a/tests/liberty/normal.lib.filtered.ok b/tests/liberty/normal.lib.filtered.ok index 757f09cab..eea7df8fe 100644 --- a/tests/liberty/normal.lib.filtered.ok +++ b/tests/liberty/normal.lib.filtered.ok @@ -6,7 +6,7 @@ library(supergate) { } pin(Y) { direction : output ; - function : A' ; + function : "A'" ; } } cell(tri_inv) { @@ -19,7 +19,7 @@ library(supergate) { } pin(Z) { direction : output ; - function : A' ; + function : "A'" ; } } cell(buffer) { @@ -29,7 +29,7 @@ library(supergate) { } pin(Y) { direction : output ; - function : A ; + function : "A" ; } } cell(nand2) { @@ -42,7 +42,7 @@ library(supergate) { } pin(Y) { direction : output ; - function : (A * B)' ; + function : "(A * B)'" ; } } cell(nor2) { @@ -55,7 +55,7 @@ library(supergate) { } pin(Y) { direction : output ; - function : (A + B)' ; + function : "(A + B)'" ; } } cell(xor2) { @@ -68,7 +68,7 @@ library(supergate) { } pin(Y) { direction : output ; - function : (A *B') + (A' * B) ; + function : "(A *B') + (A' * B)" ; } } cell(imux2) { @@ -84,16 +84,16 @@ library(supergate) { } pin(Y) { direction : output ; - function : ( (A * S) + (B * S') )' ; + function : "( (A * S) + (B * S') )'" ; } } cell(dff) { area : 6 ; - ff(IQ, IQN) { - next_state : D ; - clocked_on : CLK ; - clear : RESET ; - preset : PRESET ; + ff("IQ", "IQN") { + next_state : "D" ; + clocked_on : "CLK" ; + clear : "RESET" ; + preset : "PRESET" ; clear_preset_var1 : L ; clear_preset_var2 : L ; } @@ -111,18 +111,18 @@ library(supergate) { } pin(Q) { direction : output ; - function : IQ ; + function : "IQ" ; } pin(QN) { direction : output ; - function : IQN ; + function : "IQN" ; } } cell(latch) { area : 5 ; - latch(IQ, IQN) { - enable : G ; - data_in : D ; + latch("IQ", "IQN") { + enable : "G" ; + data_in : "D" ; } pin(D) { direction : input ; @@ -132,11 +132,11 @@ library(supergate) { } pin(Q) { direction : output ; - function : IQ ; + function : "IQ" ; } pin(QN) { direction : output ; - function : IQN ; + function : "IQN" ; } } cell(aoi211) { @@ -152,7 +152,7 @@ library(supergate) { } pin(Y) { direction : output ; - function : ((A * B) + C)' ; + function : "((A * B) + C)'" ; } } cell(oai211) { @@ -168,7 +168,7 @@ library(supergate) { } pin(Y) { direction : output ; - function : ((A + B) * C)' ; + function : "((A + B) * C)'" ; } } cell(halfadder) { @@ -181,11 +181,11 @@ library(supergate) { } pin(C) { direction : output ; - function : (A * B) ; + function : "(A * B)" ; } pin(Y) { direction : output ; - function : (A *B') + (A' * B) ; + function : "(A *B') + (A' * B)" ; } } cell(fulladder) { @@ -201,11 +201,11 @@ library(supergate) { } pin(CO) { direction : output ; - function : (((A * B)+(B * CI))+(CI * A)) ; + function : "(((A * B)+(B * CI))+(CI * A))" ; } pin(Y) { direction : output ; - function : ((A^B)^CI) ; + function : "((A^B)^CI)" ; } } } diff --git a/tests/liberty/normal.lib.verilogsim.ok b/tests/liberty/normal.lib.verilogsim.ok index 30f164a31..85aed5f4e 100644 --- a/tests/liberty/normal.lib.verilogsim.ok +++ b/tests/liberty/normal.lib.verilogsim.ok @@ -1,86 +1,86 @@ module inv (A, Y); input A; output Y; - assign Y = ~A; // A' + assign Y = ~A; // "A'" endmodule module tri_inv (A, S, Z); input A; input S; output Z; - assign Z = ~A; // A' + assign Z = ~A; // "A'" endmodule module buffer (A, Y); input A; output Y; - assign Y = A; // A + assign Y = A; // "A" endmodule module nand2 (A, B, Y); input A; input B; output Y; - assign Y = ~(A&B); // (A * B)' + assign Y = ~(A&B); // "(A * B)'" endmodule module nor2 (A, B, Y); input A; input B; output Y; - assign Y = ~(A|B); // (A + B)' + assign Y = ~(A|B); // "(A + B)'" endmodule module xor2 (A, B, Y); input A; input B; output Y; - assign Y = (A&~B)|(~A&B); // (A *B') + (A' * B) + assign Y = (A&~B)|(~A&B); // "(A *B') + (A' * B)" endmodule module imux2 (A, B, S, Y); input A; input B; input S; output Y; - assign Y = ~(&(A&S)|(B&~S)&); // ( (A * S) + (B * S') )' + assign Y = ~(&(A&S)|(B&~S)&); // "( (A * S) + (B * S') )'" endmodule module dff (D, CLK, RESET, PRESET, Q, QN); - reg IQ, IQN; + reg "IQ", "IQN"; input D; input CLK; input RESET; input PRESET; output Q; - assign Q = IQ; // IQ + assign Q = IQ; // "IQ" output QN; - assign QN = IQN; // IQN + assign QN = IQN; // "IQN" always @(posedge CLK, posedge RESET, posedge PRESET) begin if ((RESET) && (PRESET)) begin - IQ <= 0; - IQN <= 0; + "IQ" <= 0; + "IQN" <= 0; end else if (RESET) begin - IQ <= 0; - IQN <= 1; + "IQ" <= 0; + "IQN" <= 1; end else if (PRESET) begin - IQ <= 1; - IQN <= 0; + "IQ" <= 1; + "IQN" <= 0; end else begin - // D - IQ <= D; - IQN <= ~(D); + // "D" + "IQ" <= D; + "IQN" <= ~(D); end end endmodule module latch (D, G, Q, QN); - reg IQ, IQN; + reg "IQ", "IQN"; input D; input G; output Q; - assign Q = IQ; // IQ + assign Q = IQ; // "IQ" output QN; - assign QN = IQN; // IQN + assign QN = IQN; // "IQN" always @* begin if (G) begin - IQ <= D; - IQN <= ~(D); + "IQ" <= D; + "IQN" <= ~(D); end end endmodule @@ -89,29 +89,29 @@ module aoi211 (A, B, C, Y); input B; input C; output Y; - assign Y = ~((A&B)|C); // ((A * B) + C)' + assign Y = ~((A&B)|C); // "((A * B) + C)'" endmodule module oai211 (A, B, C, Y); input A; input B; input C; output Y; - assign Y = ~((A|B)&C); // ((A + B) * C)' + assign Y = ~((A|B)&C); // "((A + B) * C)'" endmodule module halfadder (A, B, C, Y); input A; input B; output C; - assign C = (A&B); // (A * B) + assign C = (A&B); // "(A * B)" output Y; - assign Y = (A&~B)|(~A&B); // (A *B') + (A' * B) + assign Y = (A&~B)|(~A&B); // "(A *B') + (A' * B)" endmodule module fulladder (A, B, CI, CO, Y); input A; input B; input CI; output CO; - assign CO = (((A&B)|(B&CI))|(CI&A)); // (((A * B)+(B * CI))+(CI * A)) + assign CO = (((A&B)|(B&CI))|(CI&A)); // "(((A * B)+(B * CI))+(CI * A))" output Y; - assign Y = ((A^B)^CI); // ((A^B)^CI) + assign Y = ((A^B)^CI); // "((A^B)^CI)" endmodule diff --git a/tests/liberty/run-test.sh b/tests/liberty/run-test.sh index ff5b20d74..8fa99d419 100755 --- a/tests/liberty/run-test.sh +++ b/tests/liberty/run-test.sh @@ -7,9 +7,10 @@ for x in *.lib; do ../../yosys-filterlib - $x 2>/dev/null > $x.filtered ../../yosys-filterlib -verilogsim $x > $x.verilogsim diff $x.filtered $x.filtered.ok && diff $x.verilogsim $x.verilogsim.ok -done +done || exit 1 for x in *.ys; do echo "Running $x.." ../../yosys -q -s $x -l ${x%.ys}.log -done +done || exit 1 + diff --git a/tests/liberty/semicolextra.lib.filtered.ok b/tests/liberty/semicolextra.lib.filtered.ok index 791b45084..10f9618cb 100644 --- a/tests/liberty/semicolextra.lib.filtered.ok +++ b/tests/liberty/semicolextra.lib.filtered.ok @@ -10,8 +10,8 @@ library(supergate) { clock : true ; } ff(IQ, IQN) { - clocked_on : CK ; - next_state : D ; + clocked_on : "CK" ; + next_state : "D" ; } pin(Q) { direction : output ; diff --git a/tests/liberty/semicolextra.lib.verilogsim.ok b/tests/liberty/semicolextra.lib.verilogsim.ok index c9eebd6ed..e3b14dbd2 100644 --- a/tests/liberty/semicolextra.lib.verilogsim.ok +++ b/tests/liberty/semicolextra.lib.verilogsim.ok @@ -4,7 +4,7 @@ module DFF (D, CK, Q); input CK; output Q; always @(posedge CK) begin - // D + // "D" IQ <= D; IQN <= ~(D); end diff --git a/tests/liberty/semicolmissing.lib.filtered.ok b/tests/liberty/semicolmissing.lib.filtered.ok index 29022cf80..2a00cc136 100644 --- a/tests/liberty/semicolmissing.lib.filtered.ok +++ b/tests/liberty/semicolmissing.lib.filtered.ok @@ -12,11 +12,11 @@ library(supergate) { } pin(CO) { direction : output ; - function : (((A * B)+(B * CI))+(CI * A)) ; + function : "(((A * B)+(B * CI))+(CI * A))" ; } pin(Y) { direction : output ; - function : ((A^B)^CI) ; + function : "((A^B)^CI)" ; } } } diff --git a/tests/liberty/semicolmissing.lib.verilogsim.ok b/tests/liberty/semicolmissing.lib.verilogsim.ok index 131ce2fdf..56d57209d 100644 --- a/tests/liberty/semicolmissing.lib.verilogsim.ok +++ b/tests/liberty/semicolmissing.lib.verilogsim.ok @@ -3,7 +3,7 @@ module fulladder (A, B, CI, CO, Y); input B; input CI; output CO; - assign CO = (((A&B)|(B&CI))|(CI&A)); // (((A * B)+(B * CI))+(CI * A)) + assign CO = (((A&B)|(B&CI))|(CI&A)); // "(((A * B)+(B * CI))+(CI * A))" output Y; - assign Y = ((A^B)^CI); // ((A^B)^CI) + assign Y = ((A^B)^CI); // "((A^B)^CI)" endmodule From 307db1ec50f800bcef6219274d83e7f40266d364 Mon Sep 17 00:00:00 2001 From: Sean Luchen Date: Thu, 3 Apr 2025 10:01:34 -0700 Subject: [PATCH 06/11] Add tests for #4976. --- tests/liberty/idranges.lib | 6 ++++++ tests/liberty/idranges.lib.filtered.ok | 2 ++ tests/liberty/idranges.lib.verilogsim.ok | 0 3 files changed, 8 insertions(+) create mode 100644 tests/liberty/idranges.lib create mode 100644 tests/liberty/idranges.lib.filtered.ok create mode 100644 tests/liberty/idranges.lib.verilogsim.ok diff --git a/tests/liberty/idranges.lib b/tests/liberty/idranges.lib new file mode 100644 index 000000000..7149f19ee --- /dev/null +++ b/tests/liberty/idranges.lib @@ -0,0 +1,6 @@ +library("foobar") { + pin("foo") { + bar : baz[0] ; + } +} + diff --git a/tests/liberty/idranges.lib.filtered.ok b/tests/liberty/idranges.lib.filtered.ok new file mode 100644 index 000000000..8a780fd67 --- /dev/null +++ b/tests/liberty/idranges.lib.filtered.ok @@ -0,0 +1,2 @@ +library("foobar") { +} diff --git a/tests/liberty/idranges.lib.verilogsim.ok b/tests/liberty/idranges.lib.verilogsim.ok new file mode 100644 index 000000000..e69de29bb From fee39a3284c90249e1d9684cf6944ffbbcbb8f90 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 9 Apr 2025 07:38:42 +0200 Subject: [PATCH 07/11] Release version 0.52 --- CHANGELOG | 13 ++++++++++++- Makefile | 4 ++-- docs/source/conf.py | 2 +- 3 files changed, 15 insertions(+), 4 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 716939992..0bbe3b179 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,8 +2,19 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.51 .. Yosys 0.52-dev +Yosys 0.51 .. Yosys 0.52 -------------------------- + * New commands and options + - Added "-pattern-limit" option to "share" pass to limit analysis effort. + - Added "libcache" pass to control caching of technology library + data parsed from liberty files. + - Added "read_verilog_file_list" to parse verilog file list. + + * Various + - Added $macc_v2 cell. + - Improve lexer performance and zlib support for "read_liberty". + - opt_expr: optimize pow of 2 cells. + Yosys 0.50 .. Yosys 0.51 -------------------------- diff --git a/Makefile b/Makefile index aafc2ceb2..15ff178ad 100644 --- a/Makefile +++ b/Makefile @@ -159,7 +159,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.51+166 +YOSYS_VER := 0.52 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2) @@ -182,7 +182,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline c4b5190.. | wc -l`/;" Makefile +# sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline c4b5190.. | wc -l`/;" Makefile ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) diff --git a/docs/source/conf.py b/docs/source/conf.py index dc7cbfe60..74ebe16e0 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -6,7 +6,7 @@ import os project = 'YosysHQ Yosys' author = 'YosysHQ GmbH' copyright ='2025 YosysHQ GmbH' -yosys_ver = "0.51" +yosys_ver = "0.52" # select HTML theme html_theme = 'furo-ys' From a2c08476678ba2c7e0a49028775ab8295b1f04bc Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 9 Apr 2025 08:21:08 +0200 Subject: [PATCH 08/11] Next dev cycle --- CHANGELOG | 3 +++ Makefile | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 0bbe3b179..413a3236c 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,9 @@ List of major changes and improvements between releases ======================================================= +Yosys 0.52 .. Yosys 0.53-dev +-------------------------- + Yosys 0.51 .. Yosys 0.52 -------------------------- * New commands and options diff --git a/Makefile b/Makefile index 15ff178ad..89723e99d 100644 --- a/Makefile +++ b/Makefile @@ -159,7 +159,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.52 +YOSYS_VER := 0.52+0 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2) @@ -182,7 +182,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: -# sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline c4b5190.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline fee39a3.. | wc -l`/;" Makefile ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) From 2443facc462355c5ad9819d2da88f04995394ab3 Mon Sep 17 00:00:00 2001 From: Emily Schmidt Date: Wed, 9 Apr 2025 10:18:25 +0100 Subject: [PATCH 09/11] add dft_tag documentation --- .../more_scripting/data_flow_tracking.rst | 71 +++++++++++++++++++ .../using_yosys/more_scripting/index.rst | 1 + 2 files changed, 72 insertions(+) create mode 100644 docs/source/using_yosys/more_scripting/data_flow_tracking.rst diff --git a/docs/source/using_yosys/more_scripting/data_flow_tracking.rst b/docs/source/using_yosys/more_scripting/data_flow_tracking.rst new file mode 100644 index 000000000..e13dfac7d --- /dev/null +++ b/docs/source/using_yosys/more_scripting/data_flow_tracking.rst @@ -0,0 +1,71 @@ +Dataflow tracking +------------------- +Yosys can be used to answer questions such as "can this signal affect this other signal?" via its *dataflow tracking* support. +For this, four special cells, ``$get_tag``, ``$set_tag``, ``$overwrite_tag`` and ``$original_tag`` are inserted into the design and then the ``dft_tag`` is run, which converts these cells into ordinary logic. +Typically, one would then use ``sby`` to prove assertions involving these cells. + +Ordinarily in Yosys, the state of a bit is simply ``0`` or ``1`` (or one of the special values, ``z`` and ``x``). +During dataflow tracking they are augmented with a set of tags. +For example, the state of a bit could be ``0`` and the set of tags ``"KEY"`` and ``"OVERFLOW"``. + +In addition to their usual operations on the logical bits, Yosys operations must now also process the status of the tags. +For this, tags are simply *forwarded* or *propagated* (i.e. copied) from inputs to outputs, according to the following general rule: + + A tag is forwarded from an input to an output if the input can affect the output, for that particular state of all other inputs. + +For example, XOR, AND and OR cells propagate tags as follows: + +#. XOR simply forwards all tags from its inputs to its output, because inputs to XOR can always affect the output. +#. AND forwards tags only if the other input is ``1``. Because if one input is ``0``, the other input can never affect the output. +#. Similarly, OR forwards tags only if the other input is ``0``. + +There are two exceptions to this rule: +#. In general, propagation is only determined approximately. + For example, unless the ``dft_tag`` code knows about a cell, it simply assumes the worst-case behaviour that all inputs can affect all outputs. + It also does not try to determine whether the effect of a signal is cancelled out, for example ``A ^ A`` or ``A ^ (B ^ A)`` is independent of ``A``, but its tags would be propagated nonetheless. +#. If tag groups are used, the rules are modified (see below). + +Because of this propagation behaviour, we can answer questions about what signals are affected by a certain signal, by injecting a tag at that point in the circuit, and observing where the tag is visible. + +Example use cases +~~~~~~~~~~~~~~~~~~ +As an example use case, consider a cryptographic processor which is not supposed to expose its secret keys to the outside world. +We can tag all key bits with the ``"KEY"`` tag and use ``sby`` to formally verify that no external signal ever carries the ``"KEY"`` tag, meaning that key information is not visible to the outside. +As a caveat, we have to manually clear the ``"KEY"`` tag during cryptographic operations, as proving that the cryptographic operations themselves do not leak key information is beyond the ability of Yosys. +However we can still easily detect, if e.g. an engineer forgot to remove debugging code that allows reading back key data. + +As a different use case, we can modify all adders in the design to set the ``"OVERFLOW"`` tag on their output bits, if the addition overflowed, and then add asserts to all flip-flop inputs and output signals that they do not carry the ``"OVERFLOW"`` tag, i.e. that the results of overflowed additions never affect system state. +Note that in this particular example we use the ability of tag insertion to be conditional on logic, in this case the overflow condition of an adder. + +Semantics of dataflow tracking cells +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +``$set_tag`` has inputs ``A``, ``SET``, ``CLR``, an output ``Y`` and a string parameter ``TAG``. +The logic value of ``A`` and all tags other than the one named by the ``TAG`` parameter are simply copied to ``Y``. +If ``SET`` is ``1``, then the named tag is added to ``Y``. +Otherwise, if ``CLR`` is ``1``, then the named tag is removed. +Otherwise, the tag is unchanged, i.e. it is present in ``Y`` if it is present in ``A``. + +``$get_tag`` has an input ``A`` and an output ``Y`` and a string parameter ``TAG``. +``$get_tag`` inspects ``A`` for the presence or absence of a tag of the given name and sets ``Y`` to ``1`` if the tag is present. +The logical value of ``A`` is completely ignored. + +``$overwrite_tag`` functions like ``$set_tag``, but lacks the ``Y`` output. +Instead of providing a modified version of the input signal, it modifies the signal ``A`` "in-place", i.e. if a signal is input to ``$overwrite_tag``, that is equivalent to interposing a ``$set_tag`` between its driver and all cells it is connected to. +The main purpose of ``$overwrite_tag`` is adding tags to signals produced within a module that cannot or should not be modified itself. + +``$original_tag`` functions identically to ``$get_tag``, but ignores ``$overwrite_tag``, i.e. when converting the ``$overwrite_tag`` to ``$set_tag`` as described above, it is equivalent to inserting the ``$get_tag`` *before* the ``$set_tag``. + +Tag groups +~~~~~~~~~~~~~~ +Tag groups are an advanced feature that modify the propagation rule discussed above. +To use tag groups, simply name tags according to the schema ``"group:name"``. +For example, ``"key:0"``, ``"key:a"``, ``"key:b"`` would be three tags in the ``"key"`` group. + +The propagation rule is then amended by + + Inputs cannot block the propagation of each other's tags for tags of the same group. + +For example, an AND gate will propagate a given tag on one input, if the other input is either 1 or carries a tag of the same group. +So if one input is ``0, "key:a"`` and the other is ``0, "key:b"`` the result would be ``0, "key:a", "key:b"``, rather than simply ``0``. +Note that if we add an unrelated ``"overflow"`` tag to the first input, it would still not be propagated. \ No newline at end of file diff --git a/docs/source/using_yosys/more_scripting/index.rst b/docs/source/using_yosys/more_scripting/index.rst index 090b9e0b9..6265e5d0e 100644 --- a/docs/source/using_yosys/more_scripting/index.rst +++ b/docs/source/using_yosys/more_scripting/index.rst @@ -12,5 +12,6 @@ More scripting selections interactive_investigation model_checking + data_flow_tracking .. troubleshooting From 32ec5a9ccd4e41f774e8bcae5fff70a568b2a36c Mon Sep 17 00:00:00 2001 From: Emily Schmidt Date: Wed, 9 Apr 2025 10:34:11 +0100 Subject: [PATCH 10/11] Revert "add dft_tag documentation" This reverts commit 2443facc462355c5ad9819d2da88f04995394ab3. --- .../more_scripting/data_flow_tracking.rst | 71 ------------------- .../using_yosys/more_scripting/index.rst | 1 - 2 files changed, 72 deletions(-) delete mode 100644 docs/source/using_yosys/more_scripting/data_flow_tracking.rst diff --git a/docs/source/using_yosys/more_scripting/data_flow_tracking.rst b/docs/source/using_yosys/more_scripting/data_flow_tracking.rst deleted file mode 100644 index e13dfac7d..000000000 --- a/docs/source/using_yosys/more_scripting/data_flow_tracking.rst +++ /dev/null @@ -1,71 +0,0 @@ -Dataflow tracking -------------------- -Yosys can be used to answer questions such as "can this signal affect this other signal?" via its *dataflow tracking* support. -For this, four special cells, ``$get_tag``, ``$set_tag``, ``$overwrite_tag`` and ``$original_tag`` are inserted into the design and then the ``dft_tag`` is run, which converts these cells into ordinary logic. -Typically, one would then use ``sby`` to prove assertions involving these cells. - -Ordinarily in Yosys, the state of a bit is simply ``0`` or ``1`` (or one of the special values, ``z`` and ``x``). -During dataflow tracking they are augmented with a set of tags. -For example, the state of a bit could be ``0`` and the set of tags ``"KEY"`` and ``"OVERFLOW"``. - -In addition to their usual operations on the logical bits, Yosys operations must now also process the status of the tags. -For this, tags are simply *forwarded* or *propagated* (i.e. copied) from inputs to outputs, according to the following general rule: - - A tag is forwarded from an input to an output if the input can affect the output, for that particular state of all other inputs. - -For example, XOR, AND and OR cells propagate tags as follows: - -#. XOR simply forwards all tags from its inputs to its output, because inputs to XOR can always affect the output. -#. AND forwards tags only if the other input is ``1``. Because if one input is ``0``, the other input can never affect the output. -#. Similarly, OR forwards tags only if the other input is ``0``. - -There are two exceptions to this rule: -#. In general, propagation is only determined approximately. - For example, unless the ``dft_tag`` code knows about a cell, it simply assumes the worst-case behaviour that all inputs can affect all outputs. - It also does not try to determine whether the effect of a signal is cancelled out, for example ``A ^ A`` or ``A ^ (B ^ A)`` is independent of ``A``, but its tags would be propagated nonetheless. -#. If tag groups are used, the rules are modified (see below). - -Because of this propagation behaviour, we can answer questions about what signals are affected by a certain signal, by injecting a tag at that point in the circuit, and observing where the tag is visible. - -Example use cases -~~~~~~~~~~~~~~~~~~ -As an example use case, consider a cryptographic processor which is not supposed to expose its secret keys to the outside world. -We can tag all key bits with the ``"KEY"`` tag and use ``sby`` to formally verify that no external signal ever carries the ``"KEY"`` tag, meaning that key information is not visible to the outside. -As a caveat, we have to manually clear the ``"KEY"`` tag during cryptographic operations, as proving that the cryptographic operations themselves do not leak key information is beyond the ability of Yosys. -However we can still easily detect, if e.g. an engineer forgot to remove debugging code that allows reading back key data. - -As a different use case, we can modify all adders in the design to set the ``"OVERFLOW"`` tag on their output bits, if the addition overflowed, and then add asserts to all flip-flop inputs and output signals that they do not carry the ``"OVERFLOW"`` tag, i.e. that the results of overflowed additions never affect system state. -Note that in this particular example we use the ability of tag insertion to be conditional on logic, in this case the overflow condition of an adder. - -Semantics of dataflow tracking cells -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -``$set_tag`` has inputs ``A``, ``SET``, ``CLR``, an output ``Y`` and a string parameter ``TAG``. -The logic value of ``A`` and all tags other than the one named by the ``TAG`` parameter are simply copied to ``Y``. -If ``SET`` is ``1``, then the named tag is added to ``Y``. -Otherwise, if ``CLR`` is ``1``, then the named tag is removed. -Otherwise, the tag is unchanged, i.e. it is present in ``Y`` if it is present in ``A``. - -``$get_tag`` has an input ``A`` and an output ``Y`` and a string parameter ``TAG``. -``$get_tag`` inspects ``A`` for the presence or absence of a tag of the given name and sets ``Y`` to ``1`` if the tag is present. -The logical value of ``A`` is completely ignored. - -``$overwrite_tag`` functions like ``$set_tag``, but lacks the ``Y`` output. -Instead of providing a modified version of the input signal, it modifies the signal ``A`` "in-place", i.e. if a signal is input to ``$overwrite_tag``, that is equivalent to interposing a ``$set_tag`` between its driver and all cells it is connected to. -The main purpose of ``$overwrite_tag`` is adding tags to signals produced within a module that cannot or should not be modified itself. - -``$original_tag`` functions identically to ``$get_tag``, but ignores ``$overwrite_tag``, i.e. when converting the ``$overwrite_tag`` to ``$set_tag`` as described above, it is equivalent to inserting the ``$get_tag`` *before* the ``$set_tag``. - -Tag groups -~~~~~~~~~~~~~~ -Tag groups are an advanced feature that modify the propagation rule discussed above. -To use tag groups, simply name tags according to the schema ``"group:name"``. -For example, ``"key:0"``, ``"key:a"``, ``"key:b"`` would be three tags in the ``"key"`` group. - -The propagation rule is then amended by - - Inputs cannot block the propagation of each other's tags for tags of the same group. - -For example, an AND gate will propagate a given tag on one input, if the other input is either 1 or carries a tag of the same group. -So if one input is ``0, "key:a"`` and the other is ``0, "key:b"`` the result would be ``0, "key:a", "key:b"``, rather than simply ``0``. -Note that if we add an unrelated ``"overflow"`` tag to the first input, it would still not be propagated. \ No newline at end of file diff --git a/docs/source/using_yosys/more_scripting/index.rst b/docs/source/using_yosys/more_scripting/index.rst index 6265e5d0e..090b9e0b9 100644 --- a/docs/source/using_yosys/more_scripting/index.rst +++ b/docs/source/using_yosys/more_scripting/index.rst @@ -12,6 +12,5 @@ More scripting selections interactive_investigation model_checking - data_flow_tracking .. troubleshooting From 33c57937cd6417dd91d34d67d6158ff550544834 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 10 Apr 2025 00:22:42 +0000 Subject: [PATCH 11/11] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index e6ac10348..deedbe17b 100644 --- a/Makefile +++ b/Makefile @@ -159,7 +159,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.52+0 +YOSYS_VER := 0.52+10 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2)