diff options
| author | Marcelina Kościelnicka <mwk@0x04.net> | 2021-02-23 12:06:21 +0100 |
|---|---|---|
| committer | Marcelina Kościelnicka <mwk@0x04.net> | 2021-02-25 22:04:04 +0100 |
| commit | 979347999f72591b5536e58110cfd491edccc937 (patch) | |
| tree | d4f44919b1223b78650cf813cfe5981a7a61d9eb /backends | |
| parent | a651204efa58b4a90ff568735e8d4f4540b92791 (diff) | |
| download | yosys-979347999f72591b5536e58110cfd491edccc937.tar.gz yosys-979347999f72591b5536e58110cfd491edccc937.tar.bz2 yosys-979347999f72591b5536e58110cfd491edccc937.zip | |
btor, smt2, smv: Add a hint on how to deal with funny FF types.
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/btor/btor.cc | 15 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 12 | ||||
| -rw-r--r-- | backends/smv/smv.cc | 18 |
3 files changed, 42 insertions, 3 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 639c6f129..692452aad 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -860,7 +860,20 @@ struct BtorWorker goto okay; } - log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell)); + if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) { + log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_btor`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + log_error("Unsupported cell type %s for cell %s.%s.\n", + log_id(cell->type), log_id(module), log_id(cell)); okay: btorf_pop(log_id(cell)); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a185fdd74..8be9e05f1 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -855,6 +855,18 @@ struct Smt2Worker return; } + if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) { + log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smt2`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } log_error("Unsupported cell type %s for cell %s.%s.\n", log_id(cell->type), log_id(module), log_id(cell)); } diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index 4e5c6050d..e41582fea 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -573,8 +573,22 @@ struct SmvWorker continue; } - if (cell->type[0] == '$') - log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell)); + if (cell->type[0] == '$') { + if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) { + log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smv`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smv`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + log_error("Unsupported cell type %s for cell %s.%s.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } // f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type)); |