APackage sysITransformConstantAcrossEquals -- APackage parameters [] -- APackage arguments clock { osc = CLK } reset { RST_N } -- APackage wire info clock info clock default_clock(CLK, {-inhigh-}); reset info reset default_reset(RST_N) clocked_by(default_clock); arg info [clockarg default_clock;, resetarg default_reset;] -- APackage clock domains [(0, [{ osc: CLK gate: 1'd1 }])] -- APackage resets [(0, { wire: RST_N })] -- AP state elements r :: ABSTRACT: Prelude.VReg = RegUN (VModInfo RegUN clock _clk__1(CLK, {-unused-}); [clockarg _clk__1;, param width;] [method (Q_OUT, [reg])read clocked_by (_clk__1) reset_by (no_reset);, method write((D_IN, [reg])) enable ((EN, [])) clocked_by (_clk__1) reset_by (no_reset);] SchedInfo [read CF read, read SB write, write SBR write] [] [] [] []) [clock { osc: CLK gate: 1'd1 }, 32'd3] [] meth types=[([], Nothing, Just (Bit 3)), ([Bit 3], Just (Bit 1), Nothing)] port types=D_IN -> Prelude.Bit 3 Q_OUT -> Prelude.Bit 3 x :: ABSTRACT: Prelude.VReg = RegUN (VModInfo RegUN clock _clk__1(CLK, {-unused-}); [clockarg _clk__1;, param width;] [method (Q_OUT, [reg])read clocked_by (_clk__1) reset_by (no_reset);, method write((D_IN, [reg])) enable ((EN, [])) clocked_by (_clk__1) reset_by (no_reset);] SchedInfo [read CF read, read SB write, write SBR write] [] [] [] []) [clock { osc: CLK gate: 1'd1 }, 32'd2] [] meth types=[([], Nothing, Just (Bit 2)), ([Bit 2], Just (Bit 1), Nothing)] port types=D_IN -> Prelude.Bit 2 Q_OUT -> Prelude.Bit 2 y :: ABSTRACT: Prelude.VReg = RegUN (VModInfo RegUN clock _clk__1(CLK, {-unused-}); [clockarg _clk__1;, param width;] [method (Q_OUT, [reg])read clocked_by (_clk__1) reset_by (no_reset);, method write((D_IN, [reg])) enable ((EN, [])) clocked_by (_clk__1) reset_by (no_reset);] SchedInfo [read CF read, read SB write, write SBR write] [] [] [] []) [clock { osc: CLK gate: 1'd1 }, 32'd2] [] meth types=[([], Nothing, Just (Bit 2)), ([Bit 2], Just (Bit 1), Nothing)] port types=D_IN -> Prelude.Bit 2 Q_OUT -> Prelude.Bit 2 z :: ABSTRACT: Prelude.VReg = RegUN (VModInfo RegUN clock _clk__1(CLK, {-unused-}); [clockarg _clk__1;, param width;] [method (Q_OUT, [reg])read clocked_by (_clk__1) reset_by (no_reset);, method write((D_IN, [reg])) enable ((EN, [])) clocked_by (_clk__1) reset_by (no_reset);] SchedInfo [read CF read, read SB write, write SBR write] [] [] [] []) [clock { osc: CLK gate: 1'd1 }, 32'd2] [] meth types=[([], Nothing, Just (Bit 2)), ([Bit 2], Just (Bit 1), Nothing)] port types=D_IN -> Prelude.Bit 2 Q_OUT -> Prelude.Bit 2 -- AP rules rule RL_Rule1 "Rule1": when True ==> { x.write ((r == 3'd2) ? x + 2'd1 : (x + 2'd2)); y.write ((r == 3'd4) ? y + 2'd1 : (y + 2'd2)); z.write ((r == 3'd7) ? z + 2'd1 : (z + 2'd2)); } rule RL_Rule2 "Rule2": when True ==> { x.write ((r == 3'd2) ? x + 2'd1 : (x + 2'd2)); y.write ((r == 3'd4) ? y + 2'd1 : (y + 2'd2)); z.write ((r == 3'd7) ? z + 2'd1 : (z + 2'd2)); } -- AP scheduling pragmas [] -- AP interface -- AP instance comments -- AP remaining proof obligations []