diff options
author | Tristan Gingold <tgingold@free.fr> | 2020-05-06 08:21:21 +0200 |
---|---|---|
committer | Tristan Gingold <tgingold@free.fr> | 2020-05-06 18:38:17 +0200 |
commit | 3b70e630543da3d42fc0cda37389312d8910e0ab (patch) | |
tree | a05f3d0030b69ecb7b3879131c5c97fd17bb10e8 /src/synth/netlists-inference.adb | |
parent | 91a8e2335d1f1b3bf3232c60d84aec94fc8f85b9 (diff) | |
download | ghdl-3b70e630543da3d42fc0cda37389312d8910e0ab.tar.gz ghdl-3b70e630543da3d42fc0cda37389312d8910e0ab.tar.bz2 ghdl-3b70e630543da3d42fc0cda37389312d8910e0ab.zip |
synth: add support for sequential assertions. Fix #1273
Diffstat (limited to 'src/synth/netlists-inference.adb')
-rw-r--r-- | src/synth/netlists-inference.adb | 151 |
1 files changed, 151 insertions, 0 deletions
diff --git a/src/synth/netlists-inference.adb b/src/synth/netlists-inference.adb index 9079a260d..7016f1f57 100644 --- a/src/synth/netlists-inference.adb +++ b/src/synth/netlists-inference.adb @@ -880,4 +880,155 @@ package body Netlists.Inference is return Res; end Infere; + + -- INST is a mux2 of a condition chain. + -- Return the input that is not 0. Could be either a mux2 or a const. + function Find_Condition_Chain_Next (Inst : Instance) return Instance + is + Mux_In0, Mux_In1 : Net; + In0_Inst, In1_Inst : Instance; + begin + Mux_In0 := Get_Input_Net (Inst, 1); + In0_Inst := Get_Net_Parent (Mux_In0); + + Mux_In1 := Get_Input_Net (Inst, 2); + In1_Inst := Get_Net_Parent (Mux_In1); + + if Get_Id (In0_Inst) /= Id_Const_UB32 then + -- The other input must be const 0. + pragma Assert (Get_Id (In1_Inst) = Id_Const_UB32 + and then Get_Param_Uns32 (In1_Inst, 0) = 0); + return In0_Inst; + else + -- Either both are const, or the other input must be const 0. + if Get_Id (In1_Inst) = Id_Const_UB32 then + -- Both are const. Return the const 1. + if Get_Param_Uns32 (In1_Inst, 0) = 0 then + pragma Assert (Get_Param_Uns32 (In0_Inst, 0) = 1); + return In0_Inst; + else + pragma Assert (Get_Param_Uns32 (In1_Inst, 0) = 1); + pragma Assert (Get_Param_Uns32 (In0_Inst, 0) = 0); + return In1_Inst; + end if; + end if; + + pragma Assert (Get_Param_Uns32 (In0_Inst, 0) = 0); + return In1_Inst; + end if; + end Find_Condition_Chain_Next; + + -- VAL is a chain of mux2 that define the conditions to enable assertions. + function Infere_Assert (Ctxt : Context_Acc; + Val : Net; + En_Gate : Net; + Stmt : Synth.Source.Syn_Src) return Net + is + Loc : constant Location_Type := Synth.Source."+" (Stmt); + Inst : Instance; + First_Inst, Last_Inst : Instance; + Clk, En : Net; + Areset : Net; + Zero : Net; + begin + -- Extract clock (if any) from VAL. Return VAL is no clock. + First_Inst := Get_Net_Parent (Val); + Inst := First_Inst; + loop + if Get_Id (Inst) /= Id_Mux2 then + pragma Assert (Get_Id (Inst) = Id_Const_UB32); + return Val; + end if; + Extract_Clock (Ctxt, Get_Input_Net (Inst, 0), Clk, En); + exit when Clk /= No_Net; + + -- No clock. Try the father. + Inst := Find_Condition_Chain_Next (Inst); + end loop; + + -- Extract enable and asynchronous reset (if any). + Last_Inst := Inst; + Areset := No_Net; + while Last_Inst /= Inst loop + declare + Cond : Net; + Next_Inst : Instance; + begin + Cond := Get_Input_Net (Inst, 0); + + -- Find the next mux. + Next_Inst := Find_Condition_Chain_Next (Inst); + + -- If the next mux is in0, negate COND. + if Next_Inst = Get_Net_Parent (Get_Input_Net (Inst, 1)) then + Cond := Build_Monadic (Ctxt, Id_Not, Cond); + Synth.Source.Set_Location (Cond, Stmt); + end if; + + -- 'And' COND to Areset. + Areset := Build2_And (Ctxt, Areset, Cond, Loc); + + Inst := Next_Inst; + end; + end loop; + + -- Same for LAST_INST, but check it is on in1. + declare + Next_Inst : Instance; + begin + Next_Inst := Find_Condition_Chain_Next (Last_Inst); + if Next_Inst /= Get_Net_Parent (Get_Input_Net (Inst, 2)) then + Error_Msg_Synth + (+Last_Inst, "assertion checked on else branch of an edge"); + return Val; + end if; + + En := Build2_And (Ctxt, En, Get_Output (Next_Inst, 0), Loc); + Zero := Get_Input_Net (Inst, 1); + end; + + -- Build an idff/iadff for each condition of the assertions. + -- The caller will connect the returned value (En) to the enable gate. + declare + En_Inp : Input; + Assert_Inp : Input; + N : Net; + Dff : Net; + begin + En_Inp := Get_First_Sink (En_Gate); + pragma Assert (En_Inp /= No_Input); + while En_Inp /= No_Input loop + -- The Enable gate is connected to an implication. + Inst := Get_Input_Parent (En_Inp); + pragma Assert (Get_Id (Inst) = Id_Not); + N := Get_Output (Inst, 0); + pragma Assert (Has_One_Connection (N)); + Inst := Get_Input_Parent (Get_First_Sink (N)); + pragma Assert (Get_Id (Inst) = Id_Or); + + N := Get_Output (Inst, 0); + pragma Assert (Has_One_Connection (N)); + Inst := Get_Input_Parent (Get_First_Sink (N)); + + pragma Assert (Get_Id (Inst) = Id_Assert); + + Assert_Inp := Get_Input (Inst, 0); + Disconnect (Assert_Inp); + + if Areset = No_Net then + Dff := Build_Idff (Ctxt, Clk, N, Zero); + else + Dff := Build_Iadff (Ctxt, Clk, N, Areset, Zero, Zero); + end if; + Set_Location (Dff, Loc); + + Connect (Assert_Inp, Dff); + + En_Inp := Get_Next_Sink (En_Inp); + end loop; + end; + + return En; + end Infere_Assert; + end Netlists.Inference; |