asyncvlsi / act

ACT hardware description language and core tools.
http://avlsi.csl.yale.edu/act
GNU General Public License v2.0
99 stars 22 forks source link

Infinite loop, likely in compute_max_reff() #14

Closed nbingham1 closed 4 years ago

nbingham1 commented 4 years ago

prs2net never completes. Likely an infinite loop in compute_max_reff()

To Reproduce Steps to reproduce the behavior:

  1. Use the ACT source included below.
  2. Run the following sequence of commands (please provide exact running instructions, preferably on Linux)
    prs2net -B -p "test<>" test.act
  3. Observe that prs2net never completes.

ACT source

export deftype globals <: int<6> (bool Vdd, GND, vpsub, vnsub, Reset, _Reset, pReset, sReset, _pReset, _sReset)
{
    sReset = Reset;
    _sReset = _Reset;
}

preal PN = 2.0;

export deftype pair <: int (bool d[2])
{
}

defproc test(globals g; pair A[4], B[4], Z, I[4], P[10])
{
    pint Na = 4;

    pint psz = 18;
    pint sz = 6;

    preal n2 = 2.0*sz;
    preal n4 = 4.0*sz;
    preal p2 = 2.0*PN*sz;
    preal p4 = 4.0*PN*sz;

    pint Dp[8];

    pair e0p, e0n, es0p, es0n, e1p, e1n, es1p, es1n;

    pint Col[Na+4];
    Col[0] = 0;
    Dp[0] = 1;
    Dp[1] = 1;
    Dp[Na+1] = 1;
    Dp[Na+2] = 1;
    Dp[Na+3] = 0;
    (i:2..Na: Dp[i] = 2; )
    (i:(Na+3): Col[i+1] = Col[i]+Dp[i]; )

    (i:Na:
        prs <g.Vdd, g.GND>
        {
            [keeper=0] passp<PN*psz>(e0p.d[0], A[i].d[1], P[Col[i]].d[1])
            [keeper=0] passn<psz>(e0p.d[1], A[i].d[1], P[Col[i]].d[1])
            [keeper=0] passp<PN*psz>(e0n.d[0], A[i].d[0], P[Col[i]].d[1])
            [keeper=0] passn<psz>(e0n.d[1], A[i].d[0], P[Col[i]].d[1])

            [keeper=0] passp<PN*psz>(es0p.d[0], A[i].d[1], P[Col[i+1]].d[1])
            [keeper=0] passn<psz>(es0p.d[1], A[i].d[1], P[Col[i+1]].d[1])
            [keeper=0] passp<PN*psz>(es0n.d[0], A[i].d[0], P[Col[i+1]].d[1])
            [keeper=0] passn<psz>(es0n.d[1], A[i].d[0], P[Col[i+1]].d[1])

            [keeper=0] passp<PN*psz>(e1p.d[0], A[i].d[1], P[Col[i+2]+Dp[i+2]-1].d[1])
            [keeper=0] passn<psz>(e1p.d[1], A[i].d[1], P[Col[i+2]+Dp[i+2]-1].d[1])
            [keeper=0] passp<PN*psz>(e1n.d[0], A[i].d[0], P[Col[i+2]+Dp[i+2]-1].d[1])
            [keeper=0] passn<psz>(e1n.d[1], A[i].d[0], P[Col[i+2]+Dp[i+2]-1].d[1])

            [keeper=0] passp<PN*psz>(es1p.d[0], A[i].d[1], P[Col[i+3]+Dp[i+3]-1].d[1])
            [keeper=0] passn<psz>(es1p.d[1], A[i].d[1], P[Col[i+3]+Dp[i+3]-1].d[1])
            [keeper=0] passp<PN*psz>(es1n.d[0], A[i].d[0], P[Col[i+3]+Dp[i+3]-1].d[1])
            [keeper=0] passn<psz>(es1n.d[1], A[i].d[0], P[Col[i+3]+Dp[i+3]-1].d[1])

            [keeper=0] passp<PN*psz>(e0p.d[0], A[i].d[0], P[Col[i]].d[0])
            [keeper=0] passn<psz>(e0p.d[1], A[i].d[0], P[Col[i]].d[0])
            [keeper=0] passp<PN*psz>(e0n.d[0], A[i].d[1], P[Col[i]].d[0])
            [keeper=0] passn<psz>(e0n.d[1], A[i].d[1], P[Col[i]].d[0])

            [keeper=0] passp<PN*psz>(es0p.d[0], A[i].d[0], P[Col[i+1]].d[0])
            [keeper=0] passn<psz>(es0p.d[1], A[i].d[0], P[Col[i+1]].d[0])
            [keeper=0] passp<PN*psz>(es0n.d[0], A[i].d[1], P[Col[i+1]].d[0])
            [keeper=0] passn<psz>(es0n.d[1], A[i].d[1], P[Col[i+1]].d[0])

            [keeper=0] passp<PN*psz>(e1p.d[0], A[i].d[0], P[Col[i+2]+Dp[i+2]-1].d[0])
            [keeper=0] passn<psz>(e1p.d[1], A[i].d[0], P[Col[i+2]+Dp[i+2]-1].d[0])
            [keeper=0] passp<PN*psz>(e1n.d[0], A[i].d[1], P[Col[i+2]+Dp[i+2]-1].d[0])
            [keeper=0] passn<psz>(e1n.d[1], A[i].d[1], P[Col[i+2]+Dp[i+2]-1].d[0])

            [keeper=0] passp<PN*psz>(es1p.d[0], A[i].d[0], P[Col[i+3]+Dp[i+3]-1].d[0])
            [keeper=0] passn<psz>(es1p.d[1], A[i].d[0], P[Col[i+3]+Dp[i+3]-1].d[0])
            [keeper=0] passp<PN*psz>(es1n.d[0], A[i].d[1], P[Col[i+3]+Dp[i+3]-1].d[0])
            [keeper=0] passn<psz>(es1n.d[1], A[i].d[1], P[Col[i+3]+Dp[i+3]-1].d[0])
        }
    )

    (i:(Na+1):
        [ i = 0 ->
                prs <g.Vdd, g.GND>
                {
                    [keeper=0] e0p.d[0]<n2> & e0n.d[0] -> P[Col[i]].d[1]-
                    [keeper=0] ~e0p.d[1]<p2> & ~e0n.d[1] -> P[Col[i]].d[0]+

                    [keeper=0] e1p.d[0]<n2> & e1n.d[0] -> P[Col[i+2]+Dp[i+2]-1].d[1]-
                    [keeper=0] ~e1p.d[1]<p2> & ~e1n.d[1] -> P[Col[i+2]+Dp[i+2]-1].d[0]+
                }
        [] i > 0 ->
            [ i = Na ->
                    prs <g.Vdd, g.GND>
                    {
                        [keeper=0] es0p.d[0]<n2> & es0n.d[0] -> P[Col[i]].d[1]-
                        [keeper=0] ~es0p.d[1]<p2> & ~es0n.d[1] -> P[Col[i]].d[0]+

                        [keeper=0] es1p.d[0]<n2> & es1n.d[0] -> P[Col[i+2]+Dp[i+2]-1].d[1]-
                        [keeper=0] ~es1p.d[1]<p2> & ~es1n.d[1] -> P[Col[i+2]+Dp[i+2]-1].d[0]+
                    }
            [] i < Na ->
                    prs <g.Vdd, g.GND>
                    {
                        [keeper=0] e0p.d[0]<n4> & e0n.d[0] & es0p.d[0] & es0n.d[0] -> P[Col[i]].d[1]-
                        [keeper=0] ~e0p.d[1]<p4> & ~e0n.d[1] & ~es0p.d[1] & ~es0n.d[1] -> P[Col[i]].d[0]+

                        [keeper=0] e1p.d[0]<n4> & e1n.d[0] & es1p.d[0] & es1n.d[0] -> P[Col[i+2]+Dp[i+2]-1].d[1]-
                        [keeper=0] ~e1p.d[1]<p4> & ~e1n.d[1] & ~es1p.d[1] & ~es1n.d[1] -> P[Col[i+2]+Dp[i+2]-1].d[0]+
                    }
            ]
        ]
    )
}

test mult;

Expected behavior prs2net should complete with the compiled spice file.

Computer setup (please complete the following information): Operating System: Red Hat Enterprise Linux Server 7.7 (Maipo) CPE OS Name: cpe:/o:redhat:enterprise_linux:7.7:GA:server Kernel: Linux 3.10.0-1062.31.2.el7.x86_64 Architecture: x86-64

g++ (GCC) 4.8.5 20150623 (Red Hat 4.8.5-39)

rmanohar commented 4 years ago

This is an NP complete problem, so a complex network could result in this issue.

nbingham1 commented 4 years ago

The network itself is not that complex. Its a set of pass transistor multiplexers driving P[]. Each element in P[] is disconnected from the others, so there should be only one path from a P[] signal to vdd or ground. Perhaps this has something to do with the templating?

Edit: Actually you may be right, the are probably connected through the pass transistors in a zig-zag pattern: P[1] to A[1] to P[2] to A[2] to ...

rmanohar commented 4 years ago

The complexity is a function of the number of unique acyclic paths in the network through source/drain connections to the power supplies, so the pass gates might make this much messier than is immediately apparent. I will take a look.

nbingham1 commented 4 years ago

Here's the graph: https://photos.app.goo.gl/F7bmPADxjQj9fBLm8

nbingham1 commented 4 years ago

"compute the maximum acyclic path from power supply to each node"

That sounds a bit like a variation on Dijkstra's or Bellman Ford?

Edit: Nope. https://en.wikipedia.org/wiki/Longest_path_problem

nbingham1 commented 4 years ago

Is "reff" only used to generate keepers?

rmanohar commented 4 years ago

Modified to stop propagating through pass gates, so this should now work properly.

nbingham1 commented 4 years ago

Yep, it works now