From d6cda1098e82a15bb905235c46992cd7de9bb690 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Thu, 4 Jul 2019 18:22:30 +0200 Subject: synth: use future states for PSL restrict directive. --- src/synth/synth-stmts.adb | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/synth/synth-stmts.adb b/src/synth/synth-stmts.adb index 9ed350e4d..cd60d4ff0 100644 --- a/src/synth/synth-stmts.adb +++ b/src/synth/synth-stmts.adb @@ -1154,7 +1154,7 @@ package body Synth.Stmts is Init : Net; Clk : Net; States : Net; - Res : Net; + Next_States : Net; begin -- create init net, clock net pragma Assert (Nbr_States <= 32); @@ -1166,13 +1166,16 @@ package body Synth.Stmts is -- create update nets -- For each state: if set, evaluate all outgoing edges. - Res := Synth_Psl_NFA (Syn_Inst, Get_PSL_NFA (Stmt), Nbr_States, States); - Connect (Get_Input (Get_Parent (States), 1), Res); + Next_States := + Synth_Psl_NFA (Syn_Inst, Get_PSL_NFA (Stmt), Nbr_States, States); + Connect (Get_Input (Get_Parent (States), 1), Next_States); - -- build assume gate + -- Build assume gate. + -- Note: for synthesis, we assume the next state will be correct. + -- (If we assume on States, then the first cycle is ignored). Build_Assume (Build_Context, Build_Reduce (Build_Context, - Netlists.Gates.Id_Red_Or, States)); + Netlists.Gates.Id_Red_Or, Next_States)); end Synth_Psl_Restrict_Directive; procedure Synth_Concurrent_Statements -- cgit v1.2.3