aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorR. Ou <rqou@robertou.com>2020-03-01 06:54:07 -0800
committerR. Ou <rqou@robertou.com>2020-03-01 16:56:21 -0800
commita6aeee4e1a41aa71d08ebac48686001ec050f973 (patch)
tree9c091fe0a81f344f10d5cd046c5d16ed5b1f6682
parent69c2d3848a3fb51887452cc52877db9d95965f11 (diff)
downloadyosys-a6aeee4e1a41aa71d08ebac48686001ec050f973.tar.gz
yosys-a6aeee4e1a41aa71d08ebac48686001ec050f973.tar.bz2
yosys-a6aeee4e1a41aa71d08ebac48686001ec050f973.zip
coolrunner2: Insert many more required feedthrough cells
-rw-r--r--techlibs/coolrunner2/coolrunner2_fixup.cc222
-rw-r--r--techlibs/coolrunner2/coolrunner2_sop.cc94
-rw-r--r--techlibs/coolrunner2/synth_coolrunner2.cc1
3 files changed, 215 insertions, 102 deletions
diff --git a/techlibs/coolrunner2/coolrunner2_fixup.cc b/techlibs/coolrunner2/coolrunner2_fixup.cc
index bc1e8ff1b..c260fafdc 100644
--- a/techlibs/coolrunner2/coolrunner2_fixup.cc
+++ b/techlibs/coolrunner2/coolrunner2_fixup.cc
@@ -23,6 +23,58 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
+RTLIL::Wire *makexorbuffer(RTLIL::Module *module, SigBit inwire)
+{
+ auto outwire = module->addWire(NEW_ID);
+
+ if (inwire == SigBit(true))
+ {
+ // Constant 1
+ auto xor_cell = module->addCell(NEW_ID, "\\MACROCELL_XOR");
+ xor_cell->setParam("\\INVERT_OUT", true);
+ xor_cell->setPort("\\OUT", outwire);
+ }
+ else if (inwire == SigBit(false))
+ {
+ // Constant 0
+ auto xor_cell = module->addCell(NEW_ID, "\\MACROCELL_XOR");
+ xor_cell->setParam("\\INVERT_OUT", false);
+ xor_cell->setPort("\\OUT", outwire);
+ }
+ else
+ {
+ auto and_to_xor_wire = module->addWire(NEW_ID);
+
+ auto and_cell = module->addCell(NEW_ID, "\\ANDTERM");
+ and_cell->setParam("\\TRUE_INP", 1);
+ and_cell->setParam("\\COMP_INP", 0);
+ and_cell->setPort("\\OUT", and_to_xor_wire);
+ and_cell->setPort("\\IN", inwire);
+ and_cell->setPort("\\IN_B", SigSpec());
+
+ auto xor_cell = module->addCell(NEW_ID, "\\MACROCELL_XOR");
+ xor_cell->setParam("\\INVERT_OUT", false);
+ xor_cell->setPort("\\IN_PTC", and_to_xor_wire);
+ xor_cell->setPort("\\OUT", outwire);
+ }
+
+ return outwire;
+}
+
+RTLIL::Wire *makeptermbuffer(RTLIL::Module *module, SigBit inwire)
+{
+ auto outwire = module->addWire(NEW_ID);
+
+ auto and_cell = module->addCell(NEW_ID, "\\ANDTERM");
+ and_cell->setParam("\\TRUE_INP", 1);
+ and_cell->setParam("\\COMP_INP", 0);
+ and_cell->setPort("\\OUT", outwire);
+ and_cell->setPort("\\IN", inwire);
+ and_cell->setPort("\\IN_B", SigSpec());
+
+ return outwire;
+}
+
struct Coolrunner2FixupPass : public Pass {
Coolrunner2FixupPass() : Pass("coolrunner2_fixup", "insert necessary buffer cells for CoolRunner-II architecture") { }
void help() YS_OVERRIDE
@@ -78,13 +130,58 @@ struct Coolrunner2FixupPass : public Pass {
}
}
- // Start by buffering FF inputs. FF inputs can only come from either
- // an IO pin or from an XOR. Otherwise AND/XOR cells need to be inserted.
+ // Find all the pterm outputs
+ pool<SigBit> sig_fed_by_pterm;
+ for (auto cell : module->selected_cells())
+ {
+ if (cell->type == "\\ANDTERM")
+ {
+ auto output = sigmap(cell->getPort("\\OUT")[0]);
+ sig_fed_by_pterm.insert(output);
+ }
+ }
+
+ // Find all the bufg outputs
+ pool<SigBit> sig_fed_by_bufg;
+ for (auto cell : module->selected_cells())
+ {
+ if (cell->type == "\\BUFG")
+ {
+ auto output = sigmap(cell->getPort("\\O")[0]);
+ sig_fed_by_bufg.insert(output);
+ }
+ }
+
+ // Find all the bufgsr outputs
+ pool<SigBit> sig_fed_by_bufgsr;
+ for (auto cell : module->selected_cells())
+ {
+ if (cell->type == "\\BUFGSR")
+ {
+ auto output = sigmap(cell->getPort("\\O")[0]);
+ sig_fed_by_bufgsr.insert(output);
+ }
+ }
+
+ // Find all the bufgts outputs
+ pool<SigBit> sig_fed_by_bufgts;
+ for (auto cell : module->selected_cells())
+ {
+ if (cell->type == "\\BUFGTS")
+ {
+ auto output = sigmap(cell->getPort("\\O")[0]);
+ sig_fed_by_bufgts.insert(output);
+ }
+ }
+
for (auto cell : module->selected_cells())
{
if (cell->type.in("\\FDCP", "\\FDCP_N", "\\FDDCP", "\\LDCP", "\\LDCP_N",
"\\FTCP", "\\FTCP_N", "\\FTDCP", "\\FDCPE", "\\FDCPE_N", "\\FDDCPE"))
{
+ // Buffering FF inputs. FF inputs can only come from either
+ // an IO pin or from an XOR. Otherwise AND/XOR cells need
+ // to be inserted.
SigBit input;
if (cell->type.in("\\FTCP", "\\FTCP_N", "\\FTDCP"))
input = sigmap(cell->getPort("\\T")[0]);
@@ -95,62 +192,115 @@ struct Coolrunner2FixupPass : public Pass {
{
log("Buffering input to \"%s\"\n", cell->name.c_str());
- auto and_to_xor_wire = module->addWire(NEW_ID);
- auto xor_to_ff_wire = module->addWire(NEW_ID);
-
- auto and_cell = module->addCell(NEW_ID, "\\ANDTERM");
- and_cell->setParam("\\TRUE_INP", 1);
- and_cell->setParam("\\COMP_INP", 0);
- and_cell->setPort("\\OUT", and_to_xor_wire);
- and_cell->setPort("\\IN", input);
- and_cell->setPort("\\IN_B", SigSpec());
-
- auto xor_cell = module->addCell(NEW_ID, "\\MACROCELL_XOR");
- xor_cell->setParam("\\INVERT_OUT", false);
- xor_cell->setPort("\\IN_PTC", and_to_xor_wire);
- xor_cell->setPort("\\OUT", xor_to_ff_wire);
+ auto xor_to_ff_wire = makexorbuffer(module, input);
if (cell->type.in("\\FTCP", "\\FTCP_N", "\\FTDCP"))
cell->setPort("\\T", xor_to_ff_wire);
else
cell->setPort("\\D", xor_to_ff_wire);
}
+
+ // Buffering FF clocks. FF clocks can only come from either
+ // a pterm or a bufg. In some cases this will be handled
+ // in coolrunner2_sop (e.g. if clock is generated from
+ // AND-ing two signals) but not in all cases.
+ SigBit clock;
+ if (cell->type.in("\\LDCP", "\\LDCP_N"))
+ clock = sigmap(cell->getPort("\\G")[0]);
+ else
+ clock = sigmap(cell->getPort("\\C")[0]);
+
+ if (!sig_fed_by_pterm[clock] && !sig_fed_by_bufg[clock])
+ {
+ log("Buffering clock to \"%s\"\n", cell->name.c_str());
+
+ auto pterm_to_ff_wire = makeptermbuffer(module, clock);
+
+ if (cell->type.in("\\LDCP", "\\LDCP_N"))
+ cell->setPort("\\G", pterm_to_ff_wire);
+ else
+ cell->setPort("\\C", pterm_to_ff_wire);
+ }
+
+ // Buffering FF set/reset. This can only come from either
+ // a pterm or a bufgsr.
+ SigBit set;
+ set = sigmap(cell->getPort("\\PRE")[0]);
+ if (set != SigBit(false))
+ {
+ if (!sig_fed_by_pterm[set] && !sig_fed_by_bufgsr[set])
+ {
+ log("Buffering set to \"%s\"\n", cell->name.c_str());
+
+ auto pterm_to_ff_wire = makeptermbuffer(module, set);
+
+ cell->setPort("\\PRE", pterm_to_ff_wire);
+ }
+ }
+
+ SigBit reset;
+ reset = sigmap(cell->getPort("\\CLR")[0]);
+ if (reset != SigBit(false))
+ {
+ if (!sig_fed_by_pterm[reset] && !sig_fed_by_bufgsr[reset])
+ {
+ log("Buffering reset to \"%s\"\n", cell->name.c_str());
+
+ auto pterm_to_ff_wire = makeptermbuffer(module, reset);
+
+ cell->setPort("\\CLR", pterm_to_ff_wire);
+ }
+ }
+
+ // Buffering FF clock enable
+ // FIXME: This doesn't fully fix PTC conflicts
+ // FIXME: Need to ensure constant enables are optimized out
+ if (cell->type.in("\\FDCPE", "\\FDCPE_N", "\\FDDCPE"))
+ {
+ SigBit ce;
+ ce = sigmap(cell->getPort("\\CE")[0]);
+ if (!sig_fed_by_pterm[ce])
+ {
+ log("Buffering clock enable to \"%s\"\n", cell->name.c_str());
+
+ auto pterm_to_ff_wire = makeptermbuffer(module, ce);
+
+ cell->setPort("\\CE", pterm_to_ff_wire);
+ }
+ }
}
}
- // Buffer IOBUFE inputs. This can only be fed from an XOR or FF.
for (auto cell : module->selected_cells())
{
if (cell->type == "\\IOBUFE")
{
+ // Buffer IOBUFE inputs. This can only be fed from an XOR or FF.
SigBit input = sigmap(cell->getPort("\\I")[0]);
- // Special case: constant 0 and 1 are handled by xc2par
- if (input == SigBit(true) || input == SigBit(false)) {
- log("Not buffering constant IO to \"%s\"\n", cell->name.c_str());
- continue;
- }
-
if (!sig_fed_by_xor[input] && !sig_fed_by_ff[input])
{
log("Buffering input to \"%s\"\n", cell->name.c_str());
- auto and_to_xor_wire = module->addWire(NEW_ID);
- auto xor_to_io_wire = module->addWire(NEW_ID);
+ auto xor_to_io_wire = makexorbuffer(module, input);
+
+ cell->setPort("\\I", xor_to_io_wire);
+ }
- auto and_cell = module->addCell(NEW_ID, "\\ANDTERM");
- and_cell->setParam("\\TRUE_INP", 1);
- and_cell->setParam("\\COMP_INP", 0);
- and_cell->setPort("\\OUT", and_to_xor_wire);
- and_cell->setPort("\\IN", input);
- and_cell->setPort("\\IN_B", SigSpec());
+ // Buffer IOBUFE enables. This can only be fed from a pterm
+ // or a bufgts.
+ if (cell->hasPort("\\E"))
+ {
+ SigBit oe;
+ oe = sigmap(cell->getPort("\\E")[0]);
+ if (!sig_fed_by_pterm[oe] && !sig_fed_by_bufgts[oe])
+ {
+ log("Buffering output enable to \"%s\"\n", cell->name.c_str());
- auto xor_cell = module->addCell(NEW_ID, "\\MACROCELL_XOR");
- xor_cell->setParam("\\INVERT_OUT", false);
- xor_cell->setPort("\\IN_PTC", and_to_xor_wire);
- xor_cell->setPort("\\OUT", xor_to_io_wire);
+ auto pterm_to_oe_wire = makeptermbuffer(module, oe);
- cell->setPort("\\I", xor_to_io_wire);
+ cell->setPort("\\E", pterm_to_oe_wire);
+ }
}
}
}
diff --git a/techlibs/coolrunner2/coolrunner2_sop.cc b/techlibs/coolrunner2/coolrunner2_sop.cc
index 49ae8e21a..c4c781939 100644
--- a/techlibs/coolrunner2/coolrunner2_sop.cc
+++ b/techlibs/coolrunner2/coolrunner2_sop.cc
@@ -108,14 +108,8 @@ struct Coolrunner2SopPass : public Pass {
}
// Check for special P-term usage
- bool is_special_pterm = false;
- bool special_pterm_can_invert = false;
- if (special_pterms_no_inv.count(sop_output) || special_pterms_inv.count(sop_output))
- {
- is_special_pterm = true;
- if (!special_pterms_no_inv[sop_output].size())
- special_pterm_can_invert = true;
- }
+ bool is_special_pterm =
+ special_pterms_no_inv.count(sop_output) || special_pterms_inv.count(sop_output);
// Construct AND cells
pool<SigBit> intermed_wires;
@@ -159,53 +153,38 @@ struct Coolrunner2SopPass : public Pass {
// Special P-term handling
if (is_special_pterm)
{
- if (!has_invert || special_pterm_can_invert)
+ // Can always connect the P-term directly if it's going
+ // into something invert-capable
+ for (auto x : special_pterms_inv[sop_output])
{
- // Can connect the P-term directly to the special term sinks
- for (auto x : special_pterms_inv[sop_output])
- std::get<0>(x)->setPort(std::get<1>(x), *intermed_wires.begin());
- for (auto x : special_pterms_no_inv[sop_output])
- std::get<0>(x)->setPort(std::get<1>(x), *intermed_wires.begin());
- }
+ std::get<0>(x)->setPort(std::get<1>(x), *intermed_wires.begin());
- if (has_invert)
- {
- if (special_pterm_can_invert)
+ // If this signal is indeed inverted, flip the cell polarity
+ if (has_invert)
{
- log_assert(special_pterms_no_inv[sop_output].size() == 0);
-
- for (auto x : special_pterms_inv[sop_output])
- {
- auto cell = std::get<0>(x);
- // Need to invert the polarity of the cell
- if (cell->type == "\\FDCP") cell->type = "\\FDCP_N";
- else if (cell->type == "\\FDCP_N") cell->type = "\\FDCP";
- else if (cell->type == "\\FTCP") cell->type = "\\FTCP_N";
- else if (cell->type == "\\FTCP_N") cell->type = "\\FTCP";
- else if (cell->type == "\\FDCPE") cell->type = "\\FDCPE_N";
- else if (cell->type == "\\FDCPE_N") cell->type = "\\FDCPE";
- else if (cell->type == "\\LDCP") cell->type = "\\LDCP_N";
- else if (cell->type == "\\LDCP_N") cell->type = "\\LDCP";
- else log_assert(!"Internal error! Bad cell type!");
- }
+ auto cell = std::get<0>(x);
+ if (cell->type == "\\FDCP") cell->type = "\\FDCP_N";
+ else if (cell->type == "\\FDCP_N") cell->type = "\\FDCP";
+ else if (cell->type == "\\FTCP") cell->type = "\\FTCP_N";
+ else if (cell->type == "\\FTCP_N") cell->type = "\\FTCP";
+ else if (cell->type == "\\FDCPE") cell->type = "\\FDCPE_N";
+ else if (cell->type == "\\FDCPE_N") cell->type = "\\FDCPE";
+ else if (cell->type == "\\LDCP") cell->type = "\\LDCP_N";
+ else if (cell->type == "\\LDCP_N") cell->type = "\\LDCP";
+ else log_assert(!"Internal error! Bad cell type!");
}
- else
- {
- // Need to construct a feed-through term
- auto feedthrough_out = module->addWire(NEW_ID);
- auto feedthrough_cell = module->addCell(NEW_ID, "\\ANDTERM");
- feedthrough_cell->setParam("\\TRUE_INP", 1);
- feedthrough_cell->setParam("\\COMP_INP", 0);
- feedthrough_cell->setPort("\\OUT", feedthrough_out);
- feedthrough_cell->setPort("\\IN", sop_output);
- feedthrough_cell->setPort("\\IN_B", SigSpec());
+ }
- for (auto x : special_pterms_inv[sop_output])
- std::get<0>(x)->setPort(std::get<1>(x), feedthrough_out);
- for (auto x : special_pterms_no_inv[sop_output])
- std::get<0>(x)->setPort(std::get<1>(x), feedthrough_out);
- }
+ // If it's going into something that's not invert-capable,
+ // connect it directly only if this signal isn't inverted
+ if (!has_invert)
+ {
+ for (auto x : special_pterms_no_inv[sop_output])
+ std::get<0>(x)->setPort(std::get<1>(x), *intermed_wires.begin());
}
+
+ // Otherwise, a feedthrough P-term has to be created. Leave that to happen
+ // in the coolrunner2_fixup pass.
}
}
else
@@ -224,23 +203,6 @@ struct Coolrunner2SopPass : public Pass {
xor_cell->setParam("\\INVERT_OUT", has_invert);
xor_cell->setPort("\\IN_ORTERM", or_to_xor_wire);
xor_cell->setPort("\\OUT", sop_output);
-
- if (is_special_pterm)
- {
- // Need to construct a feed-through term
- auto feedthrough_out = module->addWire(NEW_ID);
- auto feedthrough_cell = module->addCell(NEW_ID, "\\ANDTERM");
- feedthrough_cell->setParam("\\TRUE_INP", 1);
- feedthrough_cell->setParam("\\COMP_INP", 0);
- feedthrough_cell->setPort("\\OUT", feedthrough_out);
- feedthrough_cell->setPort("\\IN", sop_output);
- feedthrough_cell->setPort("\\IN_B", SigSpec());
-
- for (auto x : special_pterms_inv[sop_output])
- std::get<0>(x)->setPort(std::get<1>(x), feedthrough_out);
- for (auto x : special_pterms_no_inv[sop_output])
- std::get<0>(x)->setPort(std::get<1>(x), feedthrough_out);
- }
}
// Finally, remove the $sop cell
diff --git a/techlibs/coolrunner2/synth_coolrunner2.cc b/techlibs/coolrunner2/synth_coolrunner2.cc
index d940e5ac7..d5eeaf547 100644
--- a/techlibs/coolrunner2/synth_coolrunner2.cc
+++ b/techlibs/coolrunner2/synth_coolrunner2.cc
@@ -178,6 +178,7 @@ struct SynthCoolrunner2Pass : public ScriptPass
run("dffinit -ff LDCP Q INIT");
run("dffinit -ff LDCP_N Q INIT");
run("coolrunner2_sop");
+ run("clean");
run("iopadmap -bits -inpad IBUF O:I -outpad IOBUFE I:IO -inoutpad IOBUFE O:IO -toutpad IOBUFE E:I:IO -tinoutpad IOBUFE E:O:I:IO");
run("attrmvcp -attr src -attr LOC t:IOBUFE n:*");
run("attrmvcp -attr src -attr LOC -driven t:IBUF n:*");
/a> 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023
--  PSL - NFA builder.
--  Copyright (C) 2002-2016 Tristan Gingold
--
--  GHDL is free software; you can redistribute it and/or modify it under
--  the terms of the GNU General Public License as published by the Free
--  Software Foundation; either version 2, or (at your option) any later
--  version.
--
--  GHDL is distributed in the hope that it will be useful, but WITHOUT ANY
--  WARRANTY; without even the implied warranty of MERCHANTABILITY or
--  FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
--  for more details.
--
--  You should have received a copy of the GNU General Public License
--  along with GHDL; see the file COPYING.  If not, write to the Free
--  Software Foundation, 59 Temple Place - Suite 330, Boston, MA
--  02111-1307, USA.

with Tables;
with Ada.Text_IO; use Ada.Text_IO;
with Types; use Types;
with PSL.Types; use PSL.Types;
with PSL.Errors; use PSL.Errors;
with PSL.CSE; use PSL.CSE;
with PSL.QM;
with PSL.Disp_NFAs; use PSL.Disp_NFAs;
with PSL.Optimize; use PSL.Optimize;
with PSL.NFAs.Utils;
with PSL.Prints;
with PSL.NFAs; use PSL.NFAs;

package body PSL.Build is
   package Intersection is
      function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA;
   end Intersection;

   package body Intersection is

      type Stack_Entry_Id is new Natural;
      No_Stack_Entry : constant Stack_Entry_Id := 0;
      type Stack_Entry is record
         L, R : NFA_State;
         Res : NFA_State;
         Next_Unhandled : Stack_Entry_Id;
      end record;

      package Stackt is new Tables
        (Table_Component_Type => Stack_Entry,
         Table_Index_Type => Stack_Entry_Id,
         Table_Low_Bound => 1,
         Table_Initial => 128);

      First_Unhandled : Stack_Entry_Id;

      procedure Init_Stack is
      begin
         Stackt.Init;
         First_Unhandled := No_Stack_Entry;
      end Init_Stack;

      function Not_Empty return Boolean is
      begin
         return First_Unhandled /= No_Stack_Entry;
      end Not_Empty;

      procedure Pop_State (L, R : out NFA_State) is
      begin
         L := Stackt.Table (First_Unhandled).L;
         R := Stackt.Table (First_Unhandled).R;
         First_Unhandled := Stackt.Table (First_Unhandled).Next_Unhandled;
      end Pop_State;

      function Get_State (N : NFA; L, R : NFA_State) return NFA_State
      is
         Res : NFA_State;
      begin
         for I in Stackt.First .. Stackt.Last loop
            if Stackt.Table (I).L = L
              and then Stackt.Table (I).R = R
            then
               return Stackt.Table (I).Res;
            end if;
         end loop;
         Res := Add_State (N);
         Stackt.Append ((L => L, R => R, Res => Res,
                         Next_Unhandled => First_Unhandled));
         First_Unhandled := Stackt.Last;
         return Res;
      end Get_State;

      function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA
      is
         Start_L, Start_R : NFA_State;
         Final_L, Final_R : NFA_State;
         S_L, S_R : NFA_State;
         E_L, E_R : NFA_Edge;
         Res : NFA;
         Start : NFA_State;
         Extra_L, Extra_R : NFA_Edge;
      begin
         Start_L := Get_Start_State (L);
         Start_R := Get_Start_State (R);
         Final_R := Get_Final_State (R);
         Final_L := Get_Final_State (L);

         if False then
            Disp_Body (L);
            Disp_Body (R);
            Put ("//start state: ");
            Disp_State (Start_L);
            Put (",");
            Disp_State (Start_R);
            New_Line;
         end if;

         if Match_Len then
            Extra_L := No_Edge;
            Extra_R := No_Edge;
         else
            Extra_L := Add_Edge (Final_L, Final_L, True_Node);
            Extra_R := Add_Edge (Final_R, Final_R, True_Node);
         end if;

         Res := Create_NFA;
         Init_Stack;
         Start := Get_State (Res, Start_L, Start_R);
         Set_Start_State (Res, Start);

         while Not_Empty loop
            Pop_State (S_L, S_R);

            if False then
               Put ("//poped state: ");
               Disp_State (S_L);
               Put (",");
               Disp_State (S_R);
               New_Line;
            end if;

            E_L := Get_First_Src_Edge (S_L);
            while E_L /= No_Edge loop
               E_R := Get_First_Src_Edge (S_R);
               while E_R /= No_Edge loop
                  if not (E_L = Extra_L and E_R = Extra_R) then
                     Add_Edge (Get_State (Res, S_L, S_R),
                               Get_State (Res,
                                          Get_Edge_Dest (E_L),
                                          Get_Edge_Dest (E_R)),
                               Build_Bool_And (Get_Edge_Expr (E_L),
                                               Get_Edge_Expr (E_R)));
                  end if;
                  E_R := Get_Next_Src_Edge (E_R);
               end loop;
               E_L := Get_Next_Src_Edge (E_L);
            end loop;
         end loop;
         Set_Final_State (Res, Get_State (Res, Final_L, Final_R));
         Remove_Unreachable_States (Res);

         if not Match_Len then
            Remove_Edge (Extra_L);
            Remove_Edge (Extra_R);
         end if;

         --  FIXME: free L and R.
         return Res;
      end Build_Inter;
   end Intersection;

   --  All edges from A are duplicated using B as a source.
   --  Handle epsilon-edges.
   procedure Duplicate_Src_Edges (N : NFA; A, B : NFA_State)
   is
      pragma Unreferenced (N);
      E : NFA_Edge;
      Expr : Node;
      Dest : NFA_State;
   begin
      pragma Assert (A /= B);
      E := Get_First_Src_Edge (A);
      while E /= No_Edge loop
         Expr := Get_Edge_Expr (E);
         Dest := Get_Edge_Dest (E);
         if Expr /= Null_Node then
            Add_Edge (B, Dest, Expr);
         end if;
         E := Get_Next_Src_Edge (E);
      end loop;
   end Duplicate_Src_Edges;

   --  All edges to A are duplicated using B as a destination.
   --  Handle epsilon-edges.
   procedure Duplicate_Dest_Edges (N : NFA; A, B : NFA_State)
   is
      pragma Unreferenced (N);
      E : NFA_Edge;
      Expr : Node;
      Src : NFA_State;
   begin
      pragma Assert (A /= B);
      E := Get_First_Dest_Edge (A);
      while E /= No_Edge loop
         Expr := Get_Edge_Expr (E);
         Src := Get_Edge_Src (E);
         if Expr /= Null_Node then
            Add_Edge (Src, B, Expr);
         end if;
         E := Get_Next_Dest_Edge (E);
      end loop;
   end Duplicate_Dest_Edges;

   procedure Remove_Epsilon_Edge (N : NFA; S, D : NFA_State) is
   begin
      if Get_First_Src_Edge (S) = No_Edge then
         --  No edge from S.
         --  Move edges to S to D.
         Redest_Edges (S, D);
         Remove_Unconnected_State (N, S);
         if Get_Start_State (N) = S then
            Set_Start_State (N, D);
         end if;
      elsif Get_First_Dest_Edge (D) = No_Edge then
         --  No edge to D.
         --  Move edges from D to S.
         Resource_Edges (D, S);
         Remove_Unconnected_State (N, D);
         if Get_Final_State (N) = D then
            Set_Final_State (N, S);
         end if;
      else
         Duplicate_Dest_Edges (N, S, D);
         Duplicate_Src_Edges (N, D, S);
         Remove_Identical_Src_Edges (S);
      end if;
   end Remove_Epsilon_Edge;

   procedure Remove_Epsilon (N : NFA;
                             E : NFA_Edge) is
      S : constant NFA_State := Get_Edge_Src (E);
      D : constant NFA_State := Get_Edge_Dest (E);
   begin
      Remove_Edge (E);

      Remove_Epsilon_Edge (N, S, D);
   end Remove_Epsilon;

   function Build_Concat (L, R : NFA) return NFA
   is
      Start_L, Start_R : NFA_State;
      Final_L, Final_R : NFA_State;
      Eps_L, Eps_R : Boolean;
      E_L, E_R : NFA_Edge;
   begin
      Start_L := Get_Start_State (L);
      Start_R := Get_Start_State (R);
      Final_R := Get_Final_State (R);
      Final_L := Get_Final_State (L);
      Eps_L := Get_Epsilon_NFA (L);
      Eps_R := Get_Epsilon_NFA (R);

      Merge_NFA (L, R);

      Set_Start_State (L, Start_L);
      Set_Final_State (L, Final_R);
      Set_Epsilon_NFA (L, False);

      if Eps_L then
         E_L := Add_Edge (Start_L, Final_L, Null_Node);
      end if;

      if Eps_R then
         E_R := Add_Edge (Start_R, Final_R, Null_Node);
      end if;

      Remove_Epsilon_Edge (L, Final_L, Start_R);

      if Eps_L then
         Remove_Epsilon (L, E_L);
      end if;
      if Eps_R then
         Remove_Epsilon (L, E_R);
      end if;

      if (Start_L = Final_L or else Eps_L)
        and then (Start_R = Final_R or else Eps_R)
      then
         Set_Epsilon_NFA (L, True);
      end if;

      Remove_Identical_Src_Edges (Final_L);
      Remove_Identical_Dest_Edges (Start_R);

      return L;
   end Build_Concat;

   function Build_Or (L, R : NFA) return NFA
   is
      Start_L, Start_R : NFA_State;
      Final_L, Final_R : NFA_State;
      Eps : Boolean;
      Start, Final : NFA_State;
      E_S_L, E_S_R, E_L_F, E_R_F : NFA_Edge;
   begin
      Start_L := Get_Start_State (L);
      Start_R := Get_Start_State (R);
      Final_R := Get_Final_State (R);
      Final_L := Get_Final_State (L);
      Eps := Get_Epsilon_NFA (L) or Get_Epsilon_NFA (R);

      --  Optimize [*0] | R.
      if Start_L = Final_L
        and then Get_First_Src_Edge (Start_L) = No_Edge
      then
         if Start_R /= Final_R then
            Set_Epsilon_NFA (R, True);
         end if;
         --  FIXME
         --  delete_NFA (L);
         return R;
      end if;

      Merge_NFA (L, R);

      --  Use Thompson construction.
      Start := Add_State (L);
      Set_Start_State (L, Start);
      E_S_L := Add_Edge (Start, Start_L, Null_Node);
      E_S_R := Add_Edge (Start, Start_R, Null_Node);

      Final := Add_State (L);
      Set_Final_State (L, Final);
      E_L_F := Add_Edge (Final_L, Final, Null_Node);
      E_R_F := Add_Edge (Final_R, Final, Null_Node);

      Set_Epsilon_NFA (L, Eps);

      Remove_Epsilon (L, E_S_L);
      Remove_Epsilon (L, E_S_R);
      Remove_Epsilon (L, E_L_F);
      Remove_Epsilon (L, E_R_F);

      return L;
   end Build_Or;

   function Build_Fusion (L, R : NFA) return NFA
   is
      Start_R : NFA_State;
      Final_L, Final_R, S_L : NFA_State;
      E_L : NFA_Edge;
      E_R : NFA_Edge;
      N_L, Expr : Node;
   begin
      Start_R := Get_Start_State (R);
      Final_R := Get_Final_State (R);
      Final_L := Get_Final_State (L);

      Merge_NFA (L, R);

      E_L := Get_First_Dest_Edge (Final_L);
      while E_L /= No_Edge loop
         S_L := Get_Edge_Src (E_L);
         N_L := Get_Edge_Expr (E_L);

         E_R := Get_First_Src_Edge (Start_R);
         while E_R /= No_Edge loop
            Expr := Build_Bool_And (N_L, Get_Edge_Expr (E_R));
            Expr := PSL.QM.Reduce (Expr);
            if Expr /= False_Node then
               Add_Edge (S_L, Get_Edge_Dest (E_R), Expr);
            end if;
            E_R := Get_Next_Src_Edge (E_R);
         end loop;
         Remove_Identical_Src_Edges (S_L);
         E_L := Get_Next_Dest_Edge (E_L);
      end loop;

      Set_Final_State (L, Final_R);

      Set_Epsilon_NFA (L, False);

      if Get_First_Src_Edge (Final_L) = No_Edge then
         Remove_State (L, Final_L);
      end if;
      if Get_First_Dest_Edge (Start_R) = No_Edge then
         Remove_State (L, Start_R);
      end if;

      return L;
   end Build_Fusion;

   function Build_Star_Repeat (N : Node) return NFA is
      Res : NFA;
      Start, Final, S : NFA_State;
      Seq : Node;
   begin
      Seq := Get_Sequence (N);
      if Seq = Null_Node then
         --  Epsilon.
         Res := Create_NFA;
         S := Add_State (Res);
         Set_Start_State (Res, S);
         Set_Final_State (Res, S);
         return Res;
      end if;
      Res := Build_SERE_FA (Seq);
      Start := Get_Start_State (Res);
      Final := Get_Final_State (Res);
      Redest_Edges (Final, Start);
      Set_Final_State (Res, Start);
      Remove_Unconnected_State (Res, Final);
      Set_Epsilon_NFA (Res, False);
      return Res;
   end Build_Star_Repeat;

   function Build_Plus_Repeat (N : Node) return NFA is
      Res : NFA;
      Start, Final : NFA_State;
      T : NFA_Edge;
   begin
      Res := Build_SERE_FA (Get_Sequence (N));
      Start := Get_Start_State (Res);
      Final := Get_Final_State (Res);
      T := Get_First_Dest_Edge (Final);
      while T /= No_Edge loop
         Add_Edge (Get_Edge_Src (T), Start, Get_Edge_Expr (T));
         T := Get_Next_Src_Edge (T);
      end loop;
      return Res;
   end Build_Plus_Repeat;

   --  Association actual to formals, so that when a formal is referenced, the
   --  actual can be used instead.
   procedure Assoc_Instance (Decl : Node; Instance : Node)
   is
      Formal : Node;
      Actual : Node;
   begin
      --  Temporary associates actuals to formals.
      Formal := Get_Parameter_List (Decl);
      Actual := Get_Association_Chain (Instance);
      while Formal /= Null_Node loop
         if Actual = Null_Node then
            --  Not enough actual.
            raise Internal_Error;
         end if;
         if Get_Actual (Formal) /= Null_Node then
            --  Recursion
            raise Internal_Error;
         end if;
         Set_Actual (Formal, Get_Actual (Actual));
         Formal := Get_Chain (Formal);
         Actual := Get_Chain (Actual);
      end loop;
      if Actual /= Null_Node then
         --  Too many actual.
         raise Internal_Error;
      end if;
   end Assoc_Instance;

   procedure Unassoc_Instance (Decl : Node)
   is
      Formal : Node;
   begin
      --  Remove temporary association.
      Formal := Get_Parameter_List (Decl);
      while Formal /= Null_Node loop
         Set_Actual (Formal, Null_Node);
         Formal := Get_Chain (Formal);
      end loop;
   end Unassoc_Instance;

   function Build_SERE_FA (N : Node) return NFA
   is
      Res : NFA;
      S1, S2 : NFA_State;
   begin
      case Get_Kind (N) is
         when N_Booleans =>
            Res := Create_NFA;
            S1 := Add_State (Res);
            S2 := Add_State (Res);
            Set_Start_State (Res, S1);
            Set_Final_State (Res, S2);
            if N /= False_Node then
               Add_Edge (S1, S2, N);
            end if;
            return Res;
         when N_Braced_SERE =>
            return Build_SERE_FA (Get_SERE (N));
         when N_Concat_SERE =>
            return Build_Concat (Build_SERE_FA (Get_Left (N)),
                                 Build_SERE_FA (Get_Right (N)));
         when N_Fusion_SERE =>
            return Build_Fusion (Build_SERE_FA (Get_Left (N)),
                                 Build_SERE_FA (Get_Right (N)));
         when N_Match_And_Seq =>
            return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)),
                                             Build_SERE_FA (Get_Right (N)),
                                             True);
         when N_And_Seq =>
            return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)),
                                             Build_SERE_FA (Get_Right (N)),
                                             False);
         when N_Or_Prop
           | N_Or_Seq =>
            return Build_Or (Build_SERE_FA (Get_Left (N)),
                             Build_SERE_FA (Get_Right (N)));
         when N_Star_Repeat_Seq =>
            return Build_Star_Repeat (N);
         when N_Plus_Repeat_Seq =>
            return Build_Plus_Repeat (N);
         when N_Sequence_Instance
           | N_Endpoint_Instance =>
            declare
               Decl : Node;
            begin
               Decl := Get_Declaration (N);
               Assoc_Instance (Decl, N);
               Res := Build_SERE_FA (Get_Sequence (Decl));
               Unassoc_Instance (Decl);
               return Res;
            end;
         when N_Boolean_Parameter
           | N_Sequence_Parameter =>
            declare
               Actual : constant Node := Get_Actual (N);
            begin
               if Actual = Null_Node then
                  raise Internal_Error;
               end if;
               return Build_SERE_FA (Actual);
            end;
         when others =>
            Error_Kind ("build_sere_fa", N);
      end case;
   end Build_SERE_FA;

   function Count_Edges (S : NFA_State) return Natural
   is
      Res : Natural;
      E : NFA_Edge;
   begin
      Res := 0;
      E := Get_First_Src_Edge (S);
      while E /= No_Edge loop
         Res := Res + 1;
         E := Get_Next_Src_Edge (E);
      end loop;
      return Res;
   end Count_Edges;

   type Count_Vector is array (Natural range <>) of Natural;

   procedure Count_All_Edges (N : NFA; Res : out Count_Vector)
   is
      S : NFA_State;
   begin
      S := Get_First_State (N);
      while S /= No_State loop
         Res (Natural (Get_State_Label (S))) := Count_Edges (S);
         S := Get_Next_State (S);
      end loop;
   end Count_All_Edges;

   pragma Unreferenced (Count_All_Edges);

   package Determinize is
      --  Create a new NFA that reaches its final state only when N fails
      --  (ie when the final state is not reached).
      function Determinize (N : NFA) return NFA;
   end Determinize;

   package body Determinize is
      --  In all the comments N stands for the initial NFA (ie the NFA to
      --  determinize).

      use Prints;

      Flag_Trace : constant Boolean := False;
      Last_Label : Int32 := 0;

      --  The tree associates a set of states in N to *an* uniq set in the
      --  result NFA.
      --
      --  As the NFA is labelized, each node represent a state in N, and has
      --  two branches: one for state is present and one for state is absent.
      --
      --  The leaves contain the state in the result NFA.
      --
      --  The leaves are chained to create a stack of state to handle.
      --
      --  The root of the tree is node Start_Tree_Id and represent the start
      --  state of N.
      type Deter_Tree_Id is new Natural;
      No_Tree_Id : constant Deter_Tree_Id := 0;
      Start_Tree_Id : constant Deter_Tree_Id := 1;

      --  List of unhanded leaves.
      Deter_Head : Deter_Tree_Id;

      type Deter_Tree_Id_Bool_Array is array (Boolean) of Deter_Tree_Id;

      --  Node in the tree.
      type Deter_Tree_Entry is record
         Parent : Deter_Tree_Id;

         --  For non-leaf:
         Child : Deter_Tree_Id_Bool_Array;

         --  For leaf:
         Link : Deter_Tree_Id;
         State : NFA_State;
         --  + value ?
      end record;

      package Detert is new Tables
        (Table_Component_Type => Deter_Tree_Entry,
         Table_Index_Type => Deter_Tree_Id,
         Table_Low_Bound => 1,
         Table_Initial => 128);

      type Bool_Vector is array (Natural range <>) of Boolean;
      pragma Pack (Bool_Vector);

      --  Convert a set of states in N to a state in the result NFA.
      --  The set is represented by a vector of boolean.  An element of the
      --  vector is true iff the corresponding state is present.
      function Add_Vector (V : Bool_Vector; N : NFA) return NFA_State
      is
         E : Deter_Tree_Id;
         Added : Boolean;
         Res : NFA_State;
      begin
         E := Start_Tree_Id;
         Added := False;
         for I in V'Range loop
            if Detert.Table (E).Child (V (I)) = No_Tree_Id then
               Detert.Append ((Child => (No_Tree_Id, No_Tree_Id),
                               Parent => E,
                               Link => No_Tree_Id,
                               State => No_State));
               Detert.Table (E).Child (V (I)) := Detert.Last;
               E := Detert.Last;
               Added := True;
            else
               E := Detert.Table (E).Child (V (I));
               Added := False;
            end if;
         end loop;
         if Added then
            --  Create the new state.
            Res := Add_State (N);
            Detert.Table (E).State := Res;

            if Flag_Trace then
               Set_State_Label (Res, Last_Label);
               Put ("Result state" & Int32'Image (Last_Label) & " for");
               for I in V'Range loop
                  if V (I) then
                     Put (Natural'Image (I));
                  end if;
               end loop;
               New_Line;
               Last_Label := Last_Label + 1;
            end if;

            --  Put it to the list of states to be handled.
            Detert.Table (E).Link := Deter_Head;
            Deter_Head := E;

            return Res;
         else
            return Detert.Table (E).State;
         end if;
      end Add_Vector;

      --  Return true iff the stack is empty (ie all the states have been
      --  handled).
      function Stack_Empty return Boolean is
      begin
         return Deter_Head = No_Tree_Id;
      end Stack_Empty;

      --  Get an element from the stack.
      --  Extract the state in the result NFA.
      --  Rebuild the set of states in N (ie rebuild the vector of states).
      procedure Stack_Pop (V : out Bool_Vector; S : out NFA_State)
      is
         L, P : Deter_Tree_Id;
      begin
         L := Deter_Head;
         pragma Assert (L /= No_Tree_Id);
         S := Detert.Table (L).State;
         Deter_Head := Detert.Table (L).Link;

         for I in reverse V'Range loop
            pragma Assert (L /= Start_Tree_Id);
            P := Detert.Table (L).Parent;
            if L = Detert.Table (P).Child (True) then
               V (I) := True;
            elsif L = Detert.Table (P).Child (False) then
               V (I) := False;
            else
               raise Program_Error;
            end if;
            L := P;
         end loop;
         pragma Assert (L = Start_Tree_Id);
      end Stack_Pop;

      type State_Vector is array (Natural range <>) of Natural;
      type Expr_Vector is array (Natural range <>) of Node;

      procedure Build_Arcs (N : NFA;
                            State : NFA_State;
                            States : State_Vector;
                            Exprs : Expr_Vector;
                            Expr : Node;
                            V : Bool_Vector)
      is
      begin
         if Expr = False_Node then
            return;
         end if;

         if States'Length = 0 then
            declare
               Reduced_Expr : constant Node := PSL.QM.Reduce (Expr);
               --Reduced_Expr : constant Node := Expr;
               S : NFA_State;