Hi Joachim, thank you for your help. You are right, my code is generated by a tool I wrote. It basically takes a hardware description of a design in input and it produces an ECLiPSe script which describes the EFSM behaviour (i.e. state transitions) in terms of constraints. The problem with your suggestion is that I do not see a way to set up the constraints directly. The constraints related to the transitions must all be included within the for loop, and they are too specific, I see no way to write a generic predicate like the one you wrote in your example. Here is a sample of the main for loop, I hope it helps: % transition #1 (S0[J] and neg(INTERRUPT[J] #= 1 and I[J] #= 1)) => E1[J], E1[J] => (S0[J] and neg(INTERRUPT[J] #= 1 and I[J] #= 1)), (E1[J] and (S0[J] and neg(INTERRUPT[J] #= 1 and I[J] #= 1))) => (FLAG[J1] #= I[J] * 2^4 + V[J] * 2^3 + C[J] * 2^2 + Z[J] * 2^1 + N[J] * 2^0 and ADBUS[J1] #= PC[J] and I_STATUS[J1] #= 0 and INTA[J1] #= 1 and AC[J1] #= AC[J] and BYTE1[J1] #= BYTE1[J] and BYTE2[J1] #= BYTE2[J] and BYTE3[J1] #= BYTE3[J] and C[J1] #= C[J] and DATABUS_O[J1] #= DATABUS_O[J] and I[J1] #= I[J] and IAC[J1] #= IAC[J] and IBYTE1[J1] #= IBYTE1[J] and IBYTE3[J1] #= IBYTE3[J] and ICARRY[J1] #= ICARRY[J] and IDBUS[J1] #= IDBUS[J] and IPC[J1] #= IPC[J] and ITEMP[J1] #= ITEMP[J] and N[J1] #= N[J] and PC[J1] #= PC[J] and READ_MEM[J1] #= READ_MEM[J] and TEMP[J1] #= TEMP[J] and V[J1] #= V[J] and WRITE_MEM[J1] #= WRITE_MEM[J] and Z[J1] #= Z[J]), % transition #3 (S0[J] and INTERRUPT[J] #= 1 and I[J] #= 1) => E3[J], E3[J] => (S0[J] and INTERRUPT[J] #= 1 and I[J] #= 1), (E3[J] and (S0[J] and INTERRUPT[J] #= 1 and I[J] #= 1)) => (FLAG[J1] #= I[J] * 2^4 + V[J] * 2^3 + C[J] * 2^2 + Z[J] * 2^1 + N[J] * 2^0 and ADBUS[J1] #= PC[J] and I_STATUS[J1] #= 1 and INTA[J1] #= 1 and AC[J1] #= AC[J] and BYTE1[J1] #= BYTE1[J] and BYTE2[J1] #= BYTE2[J] and BYTE3[J1] #= BYTE3[J] and C[J1] #= C[J] and DATABUS_O[J1] #= DATABUS_O[J] and I[J1] #= I[J] and IAC[J1] #= IAC[J] and IBYTE1[J1] #= IBYTE1[J] and IBYTE3[J1] #= IBYTE3[J] and ICARRY[J1] #= ICARRY[J] and IDBUS[J1] #= IDBUS[J] and IPC[J1] #= IPC[J] and ITEMP[J1] #= ITEMP[J] and N[J1] #= N[J] and PC[J1] #= PC[J] and READ_MEM[J1] #= READ_MEM[J] and TEMP[J1] #= TEMP[J] and V[J1] #= V[J] and WRITE_MEM[J1] #= WRITE_MEM[J] and Z[J1] #= Z[J]), The code for other transitions is pretty similar, except for state and transitions variables (S<number> and E<number>). If you think this sample is not enough, let me know, so that I can produce the whole for loop (which is pretty large, indeed). Valerio GuarnieriReceived on Thu Apr 10 2008 - 08:44:11 CEST
This archive was generated by hypermail 2.2.0 : Thu Feb 02 2012 - 02:31:58 CET