search

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

aflat ignores exclhi and excllo #10

Closed nbingham1 closed 4 years ago

nbingham1 commented 4 years ago 
defproc test(bool a, b)
{
    spec {
        exclhi(a, b)
    }
    prs
    {
        a => b-
    }
}

test t;
$ aflat tmp.act 
"t.a"->"t.b"-
~("t.a")->"t.b"+
rmanohar commented 4 years ago

That's correct behavior. You're supposed to say mk_exclhi(a,b). The "exclhi(a,b)" is viewed as something that the circuit has to guarantee on its own (e.g. for a dualrail code).

nbingham1 commented 4 years ago

Isn't prsim supposed to issue a warning if the "exclhi" spec is violated?

rmanohar commented 4 years ago

No, they are simply stripped out for prsim, as it doesn't have any support for invariant assertions.

nbingham1 commented 4 years ago

So what are exclhi and excllo connected to then? Is it just a TODO at the moment?

rmanohar commented 4 years ago

They are used by lvp. More generally, the entire spec section will be re-done in the next year.