11:26 <Geza> Hi folks, I'm a bit of a newcomer to yosys, so apologies in advance for silly questions. I am trying to use it for some formal equivalence checking [via SymbiYosys] of some basic circuits. I can read in a gold and a gate design, and create a miter circuit, with "miter -equiv". All this works great, but I would like to add a few constraints, for

11:26 <Geza> example that the miter trigger only matters when an appropriate reset has been been performed. I can encode all these as assume/assert in a separate module that I can read in. My question is, is there a way to create an instance of this constraints module in the miter module? can use "add" and "connect" to add wires and connect everything up, but I

11:26 <Geza> can't find a way to programmatically create the constraints instance inside the yosys generated miter module.

11:26 <Geza> Any hits would be appreciated.

12:05 <ZipCPU> Geza: I'm not following the question. How is it that you are not able to create the constraints?

12:06 <ZipCPU> Are you trying to use concurrent assertions or immediate assertions?

12:07 <Geza> I have some immediate assertions in a module I wrote (well, it's auto generated but it doesn't matter at this point), which I can read in with read_verilog

12:08 <Geza> but the miter circuit created by 'miter -equiv' is created in-memory by yosys

12:09 <Geza> so what I was hoping to do is add an instance of the hand written assertions module to the in-memory mite circuit, as in SV bind

12:11 <Geza> my problem is that I can't find a way to get yosys to do that last part, i was wondering whether it is possible

12:12 <Geza> I guess I could go "write_verilog foo.v; !sed -i .. foo.v; read_verilog foo.v" but my sense of self is protesting that idea :)

12:17 <ZipCPU> Why not create your own miter circuit?

12:17 <ZipCPU> SV bind isn't supported with the open version of Yosys

12:21 <Geza> I am using this to test a compiler that outputs Verilog, so I have hundreds of examples, I was hoping I would not have to roll my own miter circuit generator, but sound like that will be the way to go, thanks for the help regardless

12:21 <ZipCPU> Which "compiler" are you using that outputs Verilog?

12:24 <Geza> This one: https://github.com/ArgonDesign/alogic it's not quite ready for public release though :)

12:24 <tpb> Title: GitHub - ArgonDesign/alogic: Alogic is a Medium Level Synthesis language for digital logic that compiles swiftly into standard Verilog-2005 for implementation in ASIC or FPGA. (at github.com)

12:29 <ZipCPU> Neat!

12:30 <Geza> Thanks, if you feel bored, you can try www.alogic.app

12:30 <ZipCPU> I think if I were bored, I'd probably start by reading the documentation ... ;)

12:32 <Geza> Haha, that would probably help!

12:33 <ZipCPU> I suppose that's an unfortunate reality of any new project. The developer sees and is focused on the internal details of how it works, whereas the newcomer is focused instead on the user interface and how its similar or different to other tools they are already familiar with

15:46 <az0re> Geza: This is currently not so easy in Yosys. What I usually do is build my own miter. But what I have recently done for the `qbfsat` command is to add an `-assume-outputs` option, which makes it easy to make this kind of multi-condition miter by just making multiple outputs. Creating the logic to test the other constraints, though, like that reset has been high, requires you to manipulate the circuit. This can either be making your own miter

15:46 <az0re> generator, or you might implement that inside e.g. the `miter` pass as an option.

15:46 <az0re> Do you have lots of different constraints you might want to add, or they are all the same for all your tests?