| *** tpb has joined #yosys | 00:00 | |
| *** emeb has quit IRC | 02:03 | |
| *** citypw has joined #yosys | 02:35 | |
| *** dh73 has joined #yosys | 02:39 | |
| *** dh73 has quit IRC | 03:23 | |
| *** Degi has quit IRC | 03:29 | |
| *** Degi_ has joined #yosys | 03:30 | |
| *** Degi_ is now known as Degi | 03:30 | |
| *** X-Scale` has joined #yosys | 03:43 | |
| *** X-Scale has quit IRC | 03:44 | |
| *** X-Scale` is now known as X-Scale | 03:44 | |
| *** futarisIRCcloud has joined #yosys | 04:05 | |
| *** X-Scale has quit IRC | 04:14 | |
| *** pacak has quit IRC | 04:17 | |
| *** pacak has joined #yosys | 04:19 | |
| *** BinaryLust has quit IRC | 04:22 | |
| *** az0re has quit IRC | 04:23 | |
| *** BinaryLust has joined #yosys | 04:27 | |
| *** FFY00 has quit IRC | 04:40 | |
| *** BinaryLust has quit IRC | 04:40 | |
| *** FFY00 has joined #yosys | 04:40 | |
| *** dys has quit IRC | 06:06 | |
| *** futarisIRCcloud has quit IRC | 06:25 | |
| *** Asu has joined #yosys | 06:36 | |
| *** az0re has joined #yosys | 06:36 | |
| *** dys has joined #yosys | 07:08 | |
| *** jakobwenzel has joined #yosys | 07:40 | |
| *** corecode has quit IRC | 07:45 | |
| *** kraiskil has joined #yosys | 08:13 | |
| *** corecode has joined #yosys | 09:56 | |
| *** dxld has joined #yosys | 09:59 | |
| *** kraiskil has quit IRC | 10:44 | |
| *** kraiskil has joined #yosys | 10:58 | |
| *** Ekho has quit IRC | 11:09 | |
| *** vidbina has joined #yosys | 11:13 | |
| *** Geza has joined #yosys | 11:13 | |
| *** Ekho has joined #yosys | 11:21 | |
| 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. | 11:26 |
| *** X-Scale has joined #yosys | 11:48 | |
| ZipCPU | Geza: I'm not following the question. How is it that you are not able to create the constraints? | 12:05 |
| ZipCPU | Are you trying to use concurrent assertions or immediate assertions? | 12:06 |
| 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:07 |
| Geza | but the miter circuit created by 'miter -equiv' is created in-memory by yosys | 12:08 |
| 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:09 |
| 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:11 |
| 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:12 |
| ZipCPU | Why not create your own miter circuit? | 12:17 |
| ZipCPU | SV bind isn't supported with the open version of Yosys | 12:17 |
| 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:21 |
| 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:24 |
| * ZipCPU takes a peek ... | 12:28 | |
| *** futarisIRCcloud has joined #yosys | 12:28 | |
| ZipCPU | Neat! | 12:29 |
| 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:30 |
| Geza | Haha, that would probably help! | 12:32 |
| 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 | 12:33 |
| *** dh73 has joined #yosys | 12:36 | |
| *** BinaryLust has joined #yosys | 12:41 | |
| *** dh73 has quit IRC | 13:02 | |
| *** citypw has quit IRC | 14:09 | |
| *** citypw has joined #yosys | 14:09 | |
| *** vidbina has quit IRC | 14:20 | |
| *** dh73 has joined #yosys | 14:42 | |
| *** jfcaron has joined #yosys | 14:45 | |
| 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? | 15:46 |
| *** emeb has joined #yosys | 15:52 | |
| *** jakobwenzel has quit IRC | 16:03 | |
| *** vidbina has joined #yosys | 16:32 | |
| *** ZipCPU has quit IRC | 16:47 | |
| *** citypw has quit IRC | 17:14 | |
| *** cr1901_modern has quit IRC | 17:18 | |
| *** _whitelogger has quit IRC | 17:21 | |
| *** _whitelogger has joined #yosys | 17:23 | |
| *** ZipCPU has joined #yosys | 17:39 | |
| *** cr1901_modern has joined #yosys | 18:07 | |
| *** dh73 has quit IRC | 18:26 | |
| *** kraiskil has quit IRC | 18:37 | |
| *** vidbina has quit IRC | 18:39 | |
| *** vidbina has joined #yosys | 18:49 | |
| *** DaKnig has quit IRC | 19:08 | |
| *** daknig has joined #yosys | 19:11 | |
| *** daknig is now known as DaKnig | 19:13 | |
| *** dh73 has joined #yosys | 19:16 | |
| *** jakobwenzel has joined #yosys | 20:24 | |
| *** vidbina has quit IRC | 20:39 | |
| *** Asuu has joined #yosys | 20:43 | |
| *** Asu has quit IRC | 20:43 | |
| *** jakobwenzel has quit IRC | 20:49 | |
| *** Geza has quit IRC | 21:18 | |
| *** jfcaron has quit IRC | 22:10 | |
| *** Asuu has quit IRC | 22:14 | |
| *** dh73 has quit IRC | 23:18 | |
| *** az0re has quit IRC | 23:43 | |
| *** _whitelogger has quit IRC | 23:48 | |
| *** _whitelogger has joined #yosys | 23:50 | |
| *** az0re has joined #yosys | 23:57 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!