Add undriven primitive

[leonardt]

Counterpart to Term which allows the user to explicitly specify a port is undriven (useful for formal verification tools where an undriven port is used to represent a value that can take on any value supplied by the tool).

[leonardt]

I think CoSA will have to add support for it, for example, Term is handled here: https://github.com/cristian-mattarei/CoSA/blob/fe06e22d26072d2f18bcf58c8e80b5a85d87c3f8/cosa/encoders/modules.py#L696-L702

CC: @makaimann does the addition of an "undriven" primitive (opposite of Term) cause any issues for CoSA? The intended use case is for formal tools to treat an undriven signal as a signal that can take on any value. For now, we could at least have CoSA error (maybe it will already do this) when it encounters this primitive. I don't think it will break any existing code since no one will be using it, and we can say this primitive is reserved for use with tools that support undriven signals.

[makaimann]

That's not a problem at all -- for us it's just an unconstrained symbol. I should be able to add support for it today! Would you be able to send me a small test case to make sure it works?

[leonardt]

Here's a test input

{"top":"global.Top",
 "namespaces":{
   "global":{
     "modules":{
       "Top":{
         "type":["Record",[
           ["O0","Bit"],
           ["O1",["Array",8,"Bit"]]
         ]],
         "instances":{
           "inst0":{
             "modref":"corebit.undriven"
           },
           "inst1":{
             "genref":"coreir.undriven",
             "genargs":{"width":["Int",8]}
           }
         },
         "connections":[
           ["self.O0","inst0.out"],
           ["self.O1","inst1.out"]
         ]
       }
     }
   }
 }
 }

It tests the bit and bit vector versions.

[leonardt]

(You'll need the master branch of coreir to use the primitive)